[opentheory-users] opentheory-users Digest, Vol 38, Issue 3

Robert White ai.robert.wangshuai at gmail.com
Fri Sep 18 15:44:04 UTC 2015

Dear Joe,

Here is the error I get when I try to export things from real.ml:

Exception: Failure "abs const out of type op definition scope: real".

Error in included file /Users/robertwhite/Projects/hol-light/real.ml

Another question is that. I noticed that you changed real_div to !x y. ~(y
= &0) ==> x / y = x * inv y

It was fun to see the original HOL Light version allowing y to be &0. So
how is that possible?

Finally, I don't know how to prove ~(&0 = &1) I find it hard to prove from
~(0 = 1). Can you give me some hint? Is that actually a subtyping or
something cos I noticed that they are of different type:

0 : num

& 0 : int

inv (&0) : real

Then how do I play with these types to get REAL_DIV_1 proved?


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150918/a2cb8a55/attachment.html>

More information about the opentheory-users mailing list