[opentheory-users] packages that are not exported in hol.ml?
ai.robert.wangshuai at gmail.com
Thu Sep 17 19:25:52 UTC 2015
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?
On 17 September 2015 at 21:21, Robert White <ai.robert.wangshuai at gmail.com>
> Dear Joe,
> > I tend to do this kind of work lazily, when someone has a
> demand for it.
> Okay, now I have demand :)
> 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
>> > (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?
>> opentheory-users mailing list
>> opentheory-users at gilith.com
> 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
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...
More information about the opentheory-users