<div dir="ltr"><div class="gmail_extra"><div class="gmail_signature"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Dear Joe,</div><div><br></div><div>Here is the error I get when I try to export things from <a href="http://real.ml">real.ml</a>:</div><div><br></div><div>







<p class=""><span class="">Exception: Failure "abs const out of type op definition scope: real".</span></p>
<p class=""><span class="">Error in included file /Users/robertwhite/Projects/hol-light/<a href="http://real.ml">real.ml</a></span></p><p class=""><span class=""><br></span></p><p class="">Another question is that. I noticed that you changed real_div to !x y. ~(y = &0) ==> x / y = x * inv y</p><p class="">It was fun to see the original HOL Light version allowing y to be &0. So how is that possible?</p><p class=""><br></p><p class="">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:</p><p class="">0 : num</p><p class="">& 0 : int</p><p class="">inv (&0) : real</p><p class=""><br></p><p class="">Then how do I play with these types to get REAL_DIV_1 proved?</p><p class="">Thanks!</p><p class="">Robert</p>







</div></div></div></div></div></div></div></div></div></div></div>
</div></div>