[opentheory-users] Error in importing

[Robert White]

Dear Joe,

Hello. I have the following errors:

# extend_the_interpretation     "opentheory/theories/list/list.int";;
val it : unit = ()
# let all= import_article "opentheory/articles/list.art";;
Exception:
Failure
 "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".

# let all= import_article "opentheory/articles/sum.art";;
Exception:
Failure
 "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".


# extend_the_interpretation     "opentheory/theories/bool/bool.int";;
Exception:
Sys_error "opentheory/theories/bool/bool.int: No such file or directory".

# extend_the_interpretation     "opentheory/theories/bool/bool.int";;
Exception:
Sys_error "opentheory/theories/bool/bool.int: No such file or directory".
# let all= import_article "opentheory/articles/bool.art";;
Exception:
Failure
 "in article opentheory/articles/bool.art at line 89: defineConst\nstack =
[Term; \"Data.Bool.T\"; Thm]\nnew_constant: constant T has already been
declared".



# let all= import_article "opentheory/articles/real.art";;
Exception:
Failure
 "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".


# let all= import_article "opentheory/articles/option.art";;
Exception:
Failure
 "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".



So far I have only the three ones you showed in previous email working. :
 "natural-divides.art", "stream.art" and "natural-prime.art"

I wonder how I should load the rest.

Thanks a lot.
-- 

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