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

[Robert White]

Dear Joe,

Thanks for the reply.

So basically I am trying to verify thing about reals. I am trying to get
the files from "calc_int.ml" to the end of hol.ml exported and verified, as
well as the libraries at /Library and /Multivariate folder.

Thanks

Robert




On 17 September 2015 at 22:10, Joe Leslie-Hurd <joe at gilith.com> wrote:

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