<div dir="ltr">Dear Joe,<div> </div><div>Thanks a lot. I just downloaded them. I will try test the whole thing again tomorrow. </div><div> </div><div>Thanks!</div><div>Robert</div></div><div class="gmail_extra"> <div class="gmail_quote">On 6 October 2015 at 23:01, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Robert, The theory lazy-list was contributed by Ramana Kumar. It was exported from HOL4 but hasn't been kept up to date with the standard theory library, so in its present state I don't think it can be imported into HOL Light. gfp is another parametric theory: $ opentheory info --theory gfp-witness 3 external type operators: -> bool natural 14 external constants: = ! /\ ==> ~ F T + bit0 bit1 odd prime suc zero 16 satisfied assumptions: hidden 1 defined constant: oddprime 2 theorems: |- odd oddprime |- prime oddprime So follow the same pattern as modular. Cheers, Joe On Tue, Oct 6, 2015 at 3:31 AM, Robert White <div class="HOEnZb"><div class="h5"><<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: > Dear Joe, > > I also have problem loading lazy-list and gfp: > > For lazy-list : > > Exception: > > Failure > > "in article lazy-list.art at line 234: const\nstack = > [\"Data.Option.NONE\"; Var; Term; Term; Term; Var; Term; Term; Var; Term; > Var; \"llist.lrep_ok\"; Var; Term; Term; [\"A\"]; \"llist.llist.rep\"; > \"llist.llist.abs\"; \"llist.llist\"; \"a0\"; \"llist.LFINITE\"; Var; Thm; > Thm]\nunknown constant \"Data.Option.NONE\"". > > > For gfp; > > > Exception: > > Failure > > "in article gfp.art at line 676: axiom\nstack = [Term; []; Thm; Thm; > Thm]\nunknown assumption:\n|- prime oddprime". > > > Could you please help on that? Thanks a lot! > > Regards > > Robert > > > > > > On 6 October 2015 at 12:15, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> > wrote: >> >> Dear Joe, >> >> I still get one error from the modular package: >> >> Exception: >> >> Failure >> >> "in article modular.art at line 11928: axiom\nstack = [Term; []; Thm; >> Thm; [[]; [[Var; Term]]]; Thm; Thm; Thm; Thm; Thm; Thm; Thm; Thm; Thm; Var; >> Thm; Thm; Thm; Thm; Thm; Var; Thm; Thm; Thm; Thm; >> [[\"Number.Modular.toNatural\"; Var]]; Term; Var; Var; >> \"Number.Modular.<=\"; Term; Var; [[]; [[Var; Term]]]; Var; Thm]\nunknown >> assumption:\n|- ~(modulus = 0)". >> >> Is there any package missing? >> >> I have loaded the following packages: >> >> stream >> >> probability >> >> natural-bits >> >> natural-divides >> >> natural-prime >> >> >> Thanks very much! >> >> >> Regards, >> >> Robert >> >> >> On 5 October 2015 at 23:27, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> >> wrote: >>> >>> Thanks very much Joe. >>> I also noticed that there is kind of dependency going on but I don't know >>> how to fix it. >>> >>> >>> On 5 October 2015 at 22:56, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote: >>>> >>>> Hi Robert, >>>> >>>> There are a couple of different obstacles here. >>>> >>>> Firstly, it is important that the dependent theories have been >>>> imported before the theory. To show all the dependent theories, use >>>> the following command: >>>> >>>> $ opentheory list --dependency-order 'Requires+ natural-prime' >>>> base-1.200 >>>> natural-divides-1.62 >>>> stream-1.46 >>>> >>>> Now this sequence will succeed: >>>> >>>> extend_the_interpretation >>>> "opentheory/theories/natural-divides/<a href="http://natural-divides.int" rel="noreferrer" target="_blank">natural-divides.int</a>";; >>>> import_article "natural-divides.art";; >>>> >>>> extend_the_interpretation >>>> "opentheory/theories/stream/<a href="http://stream.int" rel="noreferrer" target="_blank">stream.int</a>";; >>>> import_article "stream.art";; >>>> >>>> extend_the_interpretation >>>> "opentheory/theories/natural-prime/<a href="http://natural-prime.int" rel="noreferrer" target="_blank">natural-prime.int</a>";; >>>> import_article "natural-prime.art";; >>>> >>>> The second obstacle is that the theory word10 includes the theory >>>> word, which in turn includes the theory modular. So to successfully >>>> import word10 you need to extend the interpretation with the >>>> interpretations for these theories, too: >>>> >>>> $ opentheory list --dependency-order 'Requires+ word10' >>>> base-1.200 >>>> stream-1.46 >>>> probability-1.49 >>>> natural-bits-1.66 >>>> natural-divides-1.62 >>>> >>>> extend_the_interpretation >>>> "opentheory/theories/stream/<a href="http://stream.int" rel="noreferrer" target="_blank">stream.int</a>";; >>>> import_article "stream.art";; >>>> >>>> extend_the_interpretation >>>> "opentheory/theories/probability/<a href="http://probability.int" rel="noreferrer" target="_blank">probability.int</a>";; >>>> import_article "probability.art";; >>>> >>>> extend_the_interpretation >>>> "opentheory/theories/natural-bits/<a href="http://natural-bits.int" rel="noreferrer" target="_blank">natural-bits.int</a>";; >>>> import_article "natural-bits.art";; >>>> >>>> extend_the_interpretation >>>> "opentheory/theories/natural-divides/<a href="http://natural-divides.int" rel="noreferrer" target="_blank">natural-divides.int</a>";; >>>> import_article "natural-divides.art";; >>>> >>>> extend_the_interpretation >>>> "opentheory/theories/modular/<a href="http://modular.int" rel="noreferrer" target="_blank">modular.int</a>";; >>>> extend_the_interpretation >>>> "opentheory/theories/word/<a href="http://word.int" rel="noreferrer" target="_blank">word.int</a>";; >>>> extend_the_interpretation >>>> "opentheory/theories/word10/<a href="http://word10.int" rel="noreferrer" target="_blank">word10.int</a>";; >>>> import_article "word10.art";; >>>> >>>> I regard this second problem as a defect in the theories, because it's >>>> unreasonable to expect people to discover this information. I'll work >>>> on fixing it so these multiple extend_the_interpretation commands are >>>> unnecessary. >>>> >>>> Cheers, >>>> >>>> Joe >>>> >>>> On Sun, Oct 4, 2015 at 2:57 PM, Robert White >>>> <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote: >>>> > Dear Joe, >>>> > >>>> > I have problem importing article files. For example: >>>> > >>>> > Failure >>>> > >>>> > "in article word10.art at line 7495: defineConst\nstack = [Term; >>>> > \"Number.Modular.equivalent\"; Term; Var; Term; Var; []; >>>> > \"HOLLight.modular_to_class\"; \"HOLLight.modular_from_class\"; >>>> > \"Data.Word10.word10\"; TypeOp<fun>; TypeOp<fun>; Const<!>]\nunknown >>>> > constant \"Number.Modular.equivalent\"". >>>> > >>>> > I also have problems with the following packages: >>>> > >>>> > natural-prime >>>> > >>>> > gfp >>>> > >>>> > natural-fibonacci >>>> > >>>> > Could you please check if that is because opentheory packages got >>>> > updated >>>> > but the int files haven't? >>>> > >>>> > Thanks a lot. >>>> > >>>> > >>>> > -- >>>> > >>>> > Regards, >>>> > Robert >>>> > >>>> > New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>>> > New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>>> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >>>> > >>>> > >>>> > _______________________________________________ >>>> > opentheory-users mailing list >>>> > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>> > <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>>> > >>>> >>>> _______________________________________________ >>>> opentheory-users mailing list >>>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >>>> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >>> >>> >>> >>> >>> -- >>> >>> Regards, >>> Robert >>> >>> New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >>> New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >>> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >>> >> >> >> >> -- >> >> Regards, >> Robert >> >> New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> >> New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> >> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 >> > > > > -- > > Regards, > Robert > > New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a> > New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a> > Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 > > > _______________________________________________ > opentheory-users mailing list > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> > _______________________________________________ opentheory-users mailing list <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </div></div></blockquote></div> <div> </div>-- <div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div> </div><div>Regards,</div><div>Robert </div><div> </div><div>New homepage at Github: <a href="https://airobert.github.io/" target="_blank">https://airobert.github.io/</a> </div><div>New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl" style="font-size:12.8px" target="_blank">shuai.wang@student.uva.nl</a> </div><div>Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM HP: 0652691901 </div><div> </div></div></div></div></div></div></div></div></div></div></div></div> </div>