<div dir="ltr">Dear Joe,<div><br></div><div>Thanks for the reply.</div><div><br></div><div>So basically I am trying to verify thing about reals. I am trying to get the files from "<a href="http://calc_int.ml">calc_int.ml</a>" to the end of <a href="http://hol.ml">hol.ml</a> exported and verified, as well as the libraries at /Library and /Multivariate folder.</div><div><p class="">Thanks</p><p class="">Robert</p><p class=""><br></p><p class=""><br></p></div></div><div class="gmail_extra"><br><div class="gmail_quote">On 17 September 2015 at 22:10, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Robert,<br>
<br>
I don't quite understand what doesn't work - can you give an example<br>
of something that fails?<br>
<br>
Cheers,<br>
<br>
Joe<br>
<br>
On Thu, Sep 17, 2015 at 12:25 PM, Robert White<br>
<div class="HOEnZb"><div class="h5"><<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>> wrote:<br>
> Dear Joe,<br>
><br>
> One of the things that I found was that the quotient type (in short,<br>
> `:real`) can't get exported.<br>
> I am suffering from that right now.<br>
><br>
> Can you help?<br>
><br>
> Thanks<br>
> Robert<br>
><br>
> On 17 September 2015 at 21:21, Robert White <<a href="mailto:ai.robert.wangshuai@gmail.com">ai.robert.wangshuai@gmail.com</a>><br>
> wrote:<br>
>><br>
>> Dear Joe,<br>
>><br>
>> > I tend to do this kind of work lazily, when someone has a<br>
>> demand for it.<br>
>><br>
>> Okay, now I have demand :)<br>
>><br>
>> Regards,<br>
>> Robert<br>
>><br>
>><br>
>> On 17 September 2015 at 21:04, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:<br>
>>><br>
>>> Hi Robert,<br>
>>><br>
>>> > Sorry for not been "alive" for a while.<br>
>>><br>
>>> Good to have you back :-)<br>
>>><br>
>>> > I noticed that there are some files (in <a href="http://hol.ml" rel="noreferrer" target="_blank">hol.ml</a>) not exported to the<br>
>>> > base.art<br>
>>> > (mostly things about real numbers). I wonder if there is any reason for<br>
>>> > that.<br>
>>><br>
>>> The simple answer is that these files have not yet been ported to<br>
>>> OpenTheory, which involves going through each theorem and making sure<br>
>>> that it is provable using the modified HOL Light standard library that<br>
>>> precedes it. I tend to do this kind of work lazily, when someone has a<br>
>>> demand for it.<br>
>>><br>
>>> > Also, I found there is problem downloading opentheory's hol-light.<br>
>>> ><br>
>>> > $ git clone <a href="http://src.gilith.com/hol-light" rel="noreferrer" target="_blank">http://src.gilith.com/hol-light</a><br>
>>><br>
>>> It may have been a temporary connectivity issue - could you please<br>
>>> retry and let me know if you get the same result?<br>
>>><br>
>>> Cheers,<br>
>>><br>
>>> Joe<br>
>>><br>
>>> _______________________________________________<br>
>>> opentheory-users mailing list<br>
>>> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
>>> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
>><br>
>><br>
>><br>
>><br>
>> --<br>
>><br>
>> Regards,<br>
>> Robert<br>
>><br>
>> New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a><br>
>> New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a><br>
>> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901<br>
>><br>
><br>
><br>
><br>
> --<br>
><br>
> Regards,<br>
> Robert<br>
><br>
> New homepage at Github: <a href="https://airobert.github.io/" rel="noreferrer" target="_blank">https://airobert.github.io/</a><br>
> New email address at ILLC: <a href="mailto:shuai.wang@student.uva.nl">shuai.wang@student.uva.nl</a><br>
> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901<br>
><br>
><br>
> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature"><div dir="ltr"><div><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><br></div><div>Regards,</div><div>Robert </div><div><br></div><div>New homepage at Github: <a href="https://airobert.github.io/" target="_blank">https://airobert.github.io/</a><br></div><div><span style="font-size:12.8px">New email address at ILLC: </span><a href="mailto:shuai.wang@student.uva.nl" style="font-size:12.8px" target="_blank">shuai.wang@student.uva.nl</a><br></div><div><span style="font-size:12px;line-height:20px">Carolina MacGillavrylaan </span><span style="font-size:12px;line-height:20px">2246</span><span style="font-size:12px;line-height:20px"> , 1098 XK AMSTERDAM  HP: </span><span style="color:rgb(20,24,35);font-family:helvetica,arial,sans-serif;font-size:13px;line-height:17.94px;white-space:pre-wrap">0652691901</span><br></div><div><br></div></div></div></div></div></div></div></div></div></div></div></div>
</div>