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' ev
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 s
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"
Dear Thomas,
Thanks! You are right that there is no difference between "M-h M-r" and
typing in the console. I must have used some print command (which I no
longer remember the name) before to poke into the theories. I think my
script is working because pred_set and combin (the only two I am access
Dear Caballero:
Your information is very exciting for me.
For me, you are the first man who derived the division by zero and division
by zero calculus as the outputs of a computer. Meanwhile, I am writing some
book on the division by zero calculus. I would like to include the very
important i
