[opentheory-users] packages that are not exported in hol.ml?

[Joe Leslie-Hurd]

Hi Robert,

I don't quite understand what doesn't work - can you give an example
of something that fails?

Cheers,

Joe

On Thu, Sep 17, 2015 at 12:25 PM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> Dear Joe,
>
> One of the things that I found was that the quotient type (in short,
> `:real`) can't get exported.
> I am suffering from that right now.
>
> Can you help?
>
> Thanks
> Robert
>
> On 17 September 2015 at 21:21, Robert White <ai.robert.wangshuai at gmail.com>
> wrote:
>>
>> Dear Joe,
>>
>> > I tend to do this kind of work lazily, when someone has a
>> demand for it.
>>
>> Okay, now I have demand :)
>>
>> Regards,
>> Robert
>>
>>
>> On 17 September 2015 at 21:04, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>>
>>> Hi Robert,
>>>
>>> > Sorry for not been "alive" for a while.
>>>
>>> Good to have you back :-)
>>>
>>> > I noticed that there are some files (in hol.ml) not exported to the
>>> > base.art
>>> > (mostly things about real numbers). I wonder if there is any reason for
>>> > that.
>>>
>>> The simple answer is that these files have not yet been ported to
>>> OpenTheory, which involves going through each theorem and making sure
>>> that it is provable using the modified HOL Light standard library that
>>> precedes it. I tend to do this kind of work lazily, when someone has a
>>> demand for it.
>>>
>>> > Also, I found there is problem downloading opentheory's hol-light.
>>> >
>>> > $ git clone http://src.gilith.com/hol-light
>>>
>>> It may have been a temporary connectivity issue - could you please
>>> retry and let me know if you get the same result?
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> _______________________________________________
>>> opentheory-users mailing list
>>> opentheory-users at gilith.com
>>> http://www.gilith.com/opentheory/mailing-list
>>
>>
>>
>>
>> --
>>
>> Regards,
>> Robert
>>
>> New homepage at Github: https://airobert.github.io/
>> New email address at ILLC: shuai.wang at student.uva.nl
>> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
>>
>
>
>
> --
>
> Regards,
> Robert
>
> New homepage at Github: https://airobert.github.io/
> New email address at ILLC: shuai.wang at student.uva.nl
> Carolina MacGillavrylaan 2246 , 1098 XK AMSTERDAM  HP: 0652691901
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>