[opentheory-users] Question about Lazy-list

[Joe Leslie-Hurd]

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]
>