[opentheory-users] Question about Lazy-list

[Robert White]

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