<div dir="ltr">Dear Joe,<div><br></div><div>Okay, looks I have no way to load the others for now then.</div><div>I will just play with these three first. </div><div><br></div><div>Thanks again for your advice.</div><div><br></div><div>Regards,</div><div>Rob</div></div><div class="gmail_extra"><br><div class="gmail_quote">On 8 June 2015 at 17:27, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Robert,<br>
<br>
The theories that are causing you errors are part of the standard<br>
theory library:<br>
<br>
$ opentheory list 'Includes base'<br>
bool-1.36<br>
function-1.55<br>
list-1.103<br>
natural-1.104<br>
option-1.72<br>
pair-1.27<br>
real-1.61<br>
relation-1.60<br>
set-1.71<br>
sum-1.61<br>
unit-1.20<br>
<br>
Since HOL Light already implements the standard theory library, trying<br>
to reload it will generate errors about defining symbols, as you have<br>
experienced.<br>
<br>
My advice is to focus on theories that are not part of the standard<br>
theory library, the easiest to obtain being those on the OpenTheory<br>
repo:<br>
<br>
<a href="http://opentheory.gilith.com/packages/" target="_blank">http://opentheory.gilith.com/packages/</a><br>
<br>
Cheers,<br>
<br>
Joe<br>
<div class="HOEnZb"><div class="h5"><br>
On Mon, Jun 8, 2015 at 4:34 AM, Robert White<br>
<<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
> Dear Joe,<br>
><br>
> Hello. I have the following errors:<br>
><br>
> # extend_the_interpretation     "opentheory/theories/list/<a href="http://list.int" target="_blank">list.int</a>";;<br>
> val it : unit = ()<br>
> # let all= import_article "opentheory/articles/list.art";;<br>
> Exception:<br>
> Failure<br>
>  "in article opentheory/articles/list.art at line 467: defineConst\nstack =<br>
> [Term; \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var; Term; Var;<br>
> Term; Var; [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var; Var;<br>
> \"HOLLight.INJP\"; \"HOLLight.ZBOT\"; Term; Term; Term; Var; Term; Term;<br>
> Var; Term; Var; \"HOLLight.ZRECSPACE\"; [\"A\"]; \"HOLLight._dest_rec\";<br>
> \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; \"a1\"; Var; [\"A\"];<br>
> \"HOLLight._dest_list\"; \"HOLLight._mk_list\"; \"Data.List.list\";<br>
> TypeOp<fun>; \"NULL\"; \"Data.List.null\"; Var; []; Thm]\nnew_constant:<br>
> constant NUMSUM has already been declared".<br>
><br>
> # let all= import_article "opentheory/articles/sum.art";;<br>
> Exception:<br>
> Failure<br>
>  "in article opentheory/articles/sum.art at line 499: defineConst\nstack =<br>
> [Term; \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var; Term; Var;<br>
> Term; Var; [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var; Var;<br>
> \"HOLLight.INJP\"; \"HOLLight.ZBOT\"; Term; Term; Term; Var; Term; Term;<br>
> Var; Term; Var; \"HOLLight.ZRECSPACE\"; [\"A\"]; \"HOLLight._dest_rec\";<br>
> \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; Type; TypeOp<fun>; \"_15483\";<br>
> Var; Var; \"HOLLight.CONSTR\"; Var; [\"A\"; \"B\"]; \"HOLLight._dest_sum\";<br>
> \"HOLLight._mk_sum\"; \"Data.Sum.+\"; TypeOp<fun>; \"ISL\";<br>
> \"Data.Sum.isLeft\"; Var; []; Var; Thm; Thm]\nnew_constant: constant NUMSUM<br>
> has already been declared".<br>
><br>
><br>
> # extend_the_interpretation     "opentheory/theories/bool/<a href="http://bool.int" target="_blank">bool.int</a>";;<br>
> Exception:<br>
> Sys_error "opentheory/theories/bool/<a href="http://bool.int" target="_blank">bool.int</a>: No such file or directory".<br>
><br>
> # extend_the_interpretation     "opentheory/theories/bool/<a href="http://bool.int" target="_blank">bool.int</a>";;<br>
> Exception:<br>
> Sys_error "opentheory/theories/bool/<a href="http://bool.int" target="_blank">bool.int</a>: No such file or directory".<br>
> # let all= import_article "opentheory/articles/bool.art";;<br>
> Exception:<br>
> Failure<br>
>  "in article opentheory/articles/bool.art at line 89: defineConst\nstack =<br>
> [Term; \"Data.Bool.T\"; Thm]\nnew_constant: constant T has already been<br>
> declared".<br>
><br>
><br>
><br>
> # let all= import_article "opentheory/articles/real.art";;<br>
> Exception:<br>
> Failure<br>
>  "in article opentheory/articles/real.art at line 283: defineConst\nstack =<br>
> [Term; \"HOLLight.is_nadd\"; [[]; [[Var; Term]]]; [[]; [[Var; Term]]]; [];<br>
> \"HOLLight.dest_nadd\"; \"HOLLight.mk_nadd\"; \"HOLLight.nadd\";<br>
> TypeOp<fun>; \"s\"; []; \"HOLLight.dest_hreal\"; \"HOLLight.mk_hreal\";<br>
> \"HOLLight.hreal\"; TypeOp<prod>; TypeOp<fun>; TypeOp<fun>;<br>
> Const<!>]\nnew_constant: constant is_nadd has already been declared".<br>
><br>
><br>
> # let all= import_article "opentheory/articles/option.art";;<br>
> Exception:<br>
> Failure<br>
>  "in article opentheory/articles/option.art at line 478: defineConst\nstack<br>
> = [Term; \"HOLLight.NUMSUM\"; Term; Term; Term; Var; Term; Var; Term; Var;<br>
> Term; Var; [[\"HOLLight.NUMLEFT\"; Var]]; Term; Var; Var; Var; Var;<br>
> \"HOLLight.INJP\"; \"HOLLight.ZBOT\"; Term; Term; Term; Var; Term; Term;<br>
> Var; Term; Var; \"HOLLight.ZRECSPACE\"; [\"A\"]; \"HOLLight._dest_rec\";<br>
> \"HOLLight._mk_rec\"; \"HOLLight.recspace\"; Type; TypeOp<fun>; \"_15483\";<br>
> Var; Var; \"HOLLight.CONSTR\"; Var; [\"A\"]; \"HOLLight._dest_option\";<br>
> \"HOLLight._mk_option\"; \"Data.Option.option\"; TypeOp<fun>; \"is_none\";<br>
> \"Data.Option.isNone\"; Var; []; Thm]\nnew_constant: constant NUMSUM has<br>
> already been declared".<br>
><br>
><br>
><br>
> So far I have only the three ones you showed in previous email working. :<br>
> "natural-divides.art", "stream.art" and "natural-prime.art"<br>
><br>
> I wonder how I should load the rest.<br>
><br>
> Thanks a lot.<br>
> --<br>
><br>
> Regards,<br>
> Robert White (Shuai Wang)<br>
> INRIA Deducteam<br>
> [Moving to ILLC of UvA from this Sep. ]<br>
> [New email address will be <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a>]<br>
><br>
</div></div></blockquote></div><br><br clear="all"><div><br></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>