<div dir="ltr">Dear Joe,<div><br></div><div>I noticed that after reading it in, say the bool.art. We suppose to have a list of thm (of course) but I noticed there is also a list of assumptions. And the asms for bool.art is even not parsable:</div><div><br></div><div><br clear="all"><div><div> ([([], `(\a. = a (\b. = (\c. c) (\c. c))) (\d. = (\e. d e) d)`);</div><div>    ([],</div><div>     `(\a. = a (\b. = (\c. c) (\c. c)))</div><div>      (\d. (\e. = e (\f. = (\c. c) (\c. c)))</div><div>           (\g. (\h i.</div><div>                     =</div><div>                     ((\j k.</div><div>                           = (\l. l j k)</div><div>                           (\m. m (= (\c. c) (\c. c)) (= (\c. c) (\c. c))))</div><div>                      h</div><div>                     i)</div><div>                     h)</div><div>                (d g)</div><div>                (d (@ d))))`)],</div></div><div><br></div><div><br></div><div>Now I am very confused what this "asms" is here for. I can't even (meaningfully) read the first line :(</div><div><br></div><div>Thanks very much!</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>