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
> <mailto: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 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

Reply via email to