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 <[email protected]> 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
