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

[Robert White]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150917/9154a6e5/attachment-0001.html>