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

[Joe Leslie-Hurd]

Hi Robert,

I suspected that was your plan, but I didn't understand what you meant
by saying that the `:real` type couldn't be exported. The type of real
numbers is defined and exported in the realax.ml file, which is
already ported to OpenTheory.

Cheers,

Joe

On Thu, Sep 17, 2015 at 1:39 PM, Robert White
<ai.robert.wangshuai at gmail.com> wrote:
> 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
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>