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!


On Sat, Mar 2, 2019 at 3:26 PM Thomas Tuerk <> 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 <> 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.net
> _______________________________________________
> hol-info mailing list
hol-info mailing list

Reply via email to