[opentheory-users] packages that are not exported in hol.ml?
ai.robert.wangshuai at gmail.com
Thu Sep 17 19:21:51 UTC 2015
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the opentheory-users