[opentheory-users] Question about Lazy-list

[Robert White]

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/f4104b9d/attachment.html>