[opentheory-users] Question about Lazy-list

[Ramana Kumar]

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]
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150608/cff3773f/attachment.html>