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

[Robert White]

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?

Thanks!

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