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".



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 list
hol-info mailing list

Reply via email to