<div dir="ltr">Dear Joe, <div><br></div><div>Hello. I have the following errors:<div><br></div><div><div># extend_the_interpretation     "opentheory/theories/list/<a href="http://list.int">list.int</a>";;</div><div>val it : unit = ()</div><div># let all= import_article "opentheory/articles/list.art";;</div><div>Exception:</div><div>Failure</div><div> "in article opentheory/articles/list.art at line 467: defineConst\nstack = [Term; \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var; Term; Var; Term; Var; [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var; Var; \"HOLLight.INJP\"; \"HOLLight.ZBOT\"; Term; Term; Term; Var; Term; Term; Var; Term; Var; \"HOLLight.ZRECSPACE\"; [\"A\"]; \"HOLLight._dest_rec\"; \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; \"a1\"; Var; [\"A\"]; \"HOLLight._dest_list\"; \"HOLLight._mk_list\"; \"Data.List.list\"; TypeOp<fun>; \"NULL\"; \"Data.List.null\"; Var; []; Thm]\nnew_constant: constant NUMSUM has already been declared".</div></div><div><br></div><div><div># let all= import_article "opentheory/articles/sum.art";;</div><div>Exception:</div><div>Failure</div><div> "in article opentheory/articles/sum.art at line 499: defineConst\nstack = [Term; \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var; Term; Var; Term; Var; [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var; Var; \"HOLLight.INJP\"; \"HOLLight.ZBOT\"; Term; Term; Term; Var; Term; Term; Var; Term; Var; \"HOLLight.ZRECSPACE\"; [\"A\"]; \"HOLLight._dest_rec\"; \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; Type; TypeOp<fun>; \"_15483\"; Var; Var; \"HOLLight.CONSTR\"; Var; [\"A\"; \"B\"]; \"HOLLight._dest_sum\"; \"HOLLight._mk_sum\"; \"Data.Sum.+\"; TypeOp<fun>; \"ISL\"; \"Data.Sum.isLeft\"; Var; []; Var; Thm; Thm]\nnew_constant: constant NUMSUM has already been declared".</div></div><div><br></div><div><br></div><div><div># extend_the_interpretation     "opentheory/theories/bool/<a href="http://bool.int">bool.int</a>";;</div><div>Exception:</div><div>Sys_error "opentheory/theories/bool/<a href="http://bool.int">bool.int</a>: No such file or directory".</div></div><div><br></div><div><div># extend_the_interpretation     "opentheory/theories/bool/<a href="http://bool.int">bool.int</a>";;</div><div>Exception:</div><div>Sys_error "opentheory/theories/bool/<a href="http://bool.int">bool.int</a>: No such file or directory".</div><div># let all= import_article "opentheory/articles/bool.art";;</div><div>Exception:</div><div>Failure</div><div> "in article opentheory/articles/bool.art at line 89: defineConst\nstack = [Term; \"Data.Bool.T\"; Thm]\nnew_constant: constant T has already been declared".</div></div><div><br></div><div><br></div><div><br></div><div><div># let all= import_article "opentheory/articles/real.art";;</div><div>Exception:</div><div>Failure</div><div> "in article opentheory/articles/real.art at line 283: defineConst\nstack = [Term; \"HOLLight.is_nadd\"; [[]; [[Var; Term]]]; [[]; [[Var; Term]]]; []; \"HOLLight.dest_nadd\"; \"HOLLight.mk_nadd\"; \"HOLLight.nadd\"; TypeOp<fun>; \"s\"; []; \"HOLLight.dest_hreal\"; \"HOLLight.mk_hreal\"; \"HOLLight.hreal\"; TypeOp<prod>; TypeOp<fun>; TypeOp<fun>; Const<!>]\nnew_constant: constant is_nadd has already been declared".</div></div><div><br></div><div><br></div><div><div># let all= import_article "opentheory/articles/option.art";;</div><div>Exception:</div><div>Failure</div><div> "in article opentheory/articles/option.art at line 478: defineConst\nstack = [Term; \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var; Term; Var; Term; Var; [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var; Var; \"HOLLight.INJP\"; \"HOLLight.ZBOT\"; Term; Term; Term; Var; Term; Term; Var; Term; Var; \"HOLLight.ZRECSPACE\"; [\"A\"]; \"HOLLight._dest_rec\"; \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; Type; TypeOp<fun>; \"_15483\"; Var; Var; \"HOLLight.CONSTR\"; Var; [\"A\"]; \"HOLLight._dest_option\"; \"HOLLight._mk_option\"; \"Data.Option.option\"; TypeOp<fun>; \"is_none\"; \"Data.Option.isNone\"; Var; []; Thm]\nnew_constant: constant NUMSUM has already been declared".</div></div><div><br></div><div><div><br></div><div><br></div><div>So far I have only the three ones you showed in previous email working. :<span style="font-size:12.8000001907349px"> "natural-divides.art", </span><span style="font-size:12.8000001907349px">"stream.art" and </span><span style="font-size:12.8000001907349px">"natural-prime.art"</span></div><div><br></div><div>I wonder how I should load the rest.</div><div><br></div><div>Thanks a lot.</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></div>