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
