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

Reply via email to