Dear Thomas,
Thanks! You are right that there is no difference between "M-h M-r" and
typing in the console. I must have used some print command (which I no
longer remember the name) before to poke into the theories. I think my
script is working because pred_set and combin (the only two I am accessing
through the . field accessor) are loaded by default.
> ancestry "-";
val it =
["ConseqConv", "quantHeuristics", "patternMatches", "ind_type", "while",
"one", "sum", "option", "pair", "combin", "sat", "normalForms",
"relation", "min", "bool", "marker", "num", "prim_rec", "arithmetic",
"numeral", "basicSize", "numpair", "pred_set", "list", "rich_list",
"indexedLists"]: string list
It seems if I want to access other theories I need to "load namestr" first
and it is important that the name is a string and not a label.
Thanks for the help!
Haitao
On Sat, Mar 2, 2019 at 3:26 PM Thomas Tuerk <tho...@tuerk-brechen.de> wrote:
> Dear Haito,
>
> what are you trying to do? HOL theories are ML modules. If you type a
> value, the Polyml REPL replies the value. However, as your error message
> correctly states, modules are not values. So, the error is what I expect
> and not a sign that a module is no longer visible.
>
> So, "combinTheory" is a (known and loaded) module and you get an error.
> "combineTheory.K_DEF" is a value (of type thm) and it works. I does not
> make sense to me that you say it works in the emacs mode though. There are
> a few hacks in of loading and opening modules, but nothing that should lead
> to the behaviour you describe (as far as I'm aware). For me, I get the same
> error also within emacs. I do not have a recent version of HOL installed
> currently, though.
>
> By the way, it is not HOL theory specific. Try e.g. the module "List" and
> "List.hd". For opening a module you need to use "open".
>
> Best
>
> Thomas
>
>
> On 03.03.19 00:06, Haitao Zhang wrote:
>
> And even more weird:
>
> > combinTheory;
> poly: : error: Value or constructor (combinTheory) has not been declared
> Found near combinTheory
> Static Errors
> > combinTheory.K_DEF;
> val it = ⊢ K = (λx y. x): thm
>
> Hmm?!
>
> On Sat, Mar 2, 2019 at 2:34 PM Haitao Zhang <zhtp...@gmail.com> wrote:
>
>> For some reason in my hol session system libraries are no longer visible.
>> If I directly type into the hol console:
>>
>> > pred_setTheory;
>> poly: : error: Value or constructor (pred_setTheory) has not been declared
>> Found near pred_setTheory
>> Static Errors
>>
>> But when I evaluates through emacs 'M-h' 'M-r' everything still works.
>> The only difference I can tell is that in the emacs case hol is reading and
>> evaluating a temporarily created script sml file.
>>
>> I definitely remember I could do the above in the hol console as well and
>> I had not played with any settings/env variables intentionally. It is
>> possible that sometimes by hitting the wrong key sequence in emacs I had
>> sent very erroneous strings to be evaluated.
>>
>> Where should I look to resolve this?
>>
>> Thanks,
>> Haitao
>>
>
>
> _______________________________________________
> hol-info mailing
> listhol-info@lists.sourceforge.nethttps://lists.sourceforge.net/lists/listinfo/hol-info
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
