[opentheory-users] Error in importing

[Robert White]

Dear Joe,

Okay, looks I have no way to load the others for now then.
I will just play with these three first.

Thanks again for your advice.

Regards,
Rob

On 8 June 2015 at 17:27, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Robert,
>
> The theories that are causing you errors are part of the standard
> theory library:
>
> $ opentheory list 'Includes base'
> bool-1.36
> function-1.55
> list-1.103
> natural-1.104
> option-1.72
> pair-1.27
> real-1.61
> relation-1.60
> set-1.71
> sum-1.61
> unit-1.20
>
> Since HOL Light already implements the standard theory library, trying
> to reload it will generate errors about defining symbols, as you have
> experienced.
>
> My advice is to focus on theories that are not part of the standard
> theory library, the easiest to obtain being those on the OpenTheory
> repo:
>
> http://opentheory.gilith.com/packages/
>
> Cheers,
>
> Joe
>
> On Mon, Jun 8, 2015 at 4:34 AM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
> > 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 (Shuai Wang)
> > INRIA Deducteam
> > [Moving to ILLC of UvA from this Sep. ]
> > [New email address will be shuai.wang at student.uva.nl]
> >
>



-- 

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/31d89dd3/attachment-0001.html>