<div dir="ltr">Dear Joe and Ramana,<div><br></div><div>I used the new Holide and dedukti for proof checking of the whole Opentheory repos. There is one good news and one bad news.</div><div><br></div><div>The good news is:</div><div><br></div><div>I have checked through the whole library of the rest apart from lazy-list without problems. They all passed the checking. </div><div><br></div><div>The bad news is:<br></div><div><br></div><div>lazy-list didn't pass the check. </div><div><br></div><div>--------this is the error line by Dedukti --------------------------------</div><div><div><div>Processing file 'dedukti/<a href="http://lazy-list.dk">lazy-list.dk</a>'...</div><div>ERROR line:106697 column:149 Cannot find symbol 'lazy_2Dlist.A'.</div></div><div><br></div><div>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.</div><div><br></div><div>Thanks!</div>-- <br><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><br></div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div><div>[Moving to ILLC of UvA from this Sep. ]</div><div>[New email address will be <a href="mailto:shuai.wang@student.uva.nl" target="_blank">shuai.wang@student.uva.nl</a>]</div><div><br></div></div></div></div></div></div></div></div></div></div></div>
</div></div>