[opentheory-users] Question about Lazy-list

[Robert White]

Dear Ramana,

I am not sure how to deal with it. Do you have any advice please. I am not
familiar with generating / extracting *.art files. Neither debugging though
a .art file.

Thanks

On 8 June 2015 at 17:36, Ramana Kumar <ramana at member.fsf.org> wrote:

> The lazy-list package is based on a HOL4 theory of lazy lists, which can
> be found here:
> https://github.com/HOL-Theorem-Prover/HOL/tree/master/src/llist.
>
> On 8 June 2015 at 16:33, Robert White <ai.robert.wangshuai at gmail.com>
> wrote:
>
>> Thanks Joe,
>>
>> I will wait for further updates then.
>>
>> Regards,
>> Robert
>>
>> On 8 June 2015 at 17:31, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>
>>> Hi Robert,
>>>
>>> In terms of the OpenTheory package, you are correct that lazy-list is
>>> monolithic:
>>>
>>> $ opentheory info --theory-source lazy-list
>>> main {
>>>   article: "llist.art"
>>> }
>>>
>>> However, Ramana may be able to dig up source files for the article
>>> that could be restructured into subpackages.
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> On Mon, Jun 8, 2015 at 2:44 AM, Robert White
>>> <ai.robert.wangshuai at gmail.com> wrote:
>>> > Dear Joe and Ramana,
>>> >
>>> > I used the new Holide and dedukti for proof checking of the whole
>>> Opentheory
>>> > repos. There is one good news and one bad news.
>>> >
>>> > The good news is:
>>> >
>>> > I have checked through the whole library of the rest apart from
>>> lazy-list
>>> > without problems. They all passed the checking.
>>> >
>>> > The bad news is:
>>> >
>>> > lazy-list didn't pass the check.
>>> >
>>> > --------this is the error line by Dedukti
>>> --------------------------------
>>> > Processing file 'dedukti/lazy-list.dk'...
>>> > ERROR line:106697 column:149 Cannot find symbol 'lazy_2Dlist.A'.
>>> >
>>> > I searched online and found there isn't sub-packages for me to check
>>> > individually. I wonder if this one is just as a big whole file or
>>> maybe I
>>> > can somehow unpack it to different files and check through each
>>> > individually.
>>> >
>>> > Thanks!
>>> > --
>>> >
>>> > Regards,
>>> > Robert White (Shuai Wang)
>>> > INRIA Deducteam
>>> > [Moving to ILLC of UvA from this Sep. ]
>>> > [New email address will be shuai.wang at student.uva.nl]
>>> >
>>>
>>
>>
>>
>> --
>>
>> Regards,
>> Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
>> INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
>> [Moving to ILLC of UvA from this Sep. ]
>> [New email address will be shuai.wang at student.uva.nl]
>>
>>
>


-- 

Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
[Moving to ILLC of UvA from this Sep. ]
[New email address will be shuai.wang at student.uva.nl]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150608/353e3d06/attachment.html>