[opentheory-users] interesting articles

[Joe Hurd]

Hi Ramana,

[I'm replying to the OpenTheory mailing list, since I think your
question is of general interest.]

I am currently working on some example HOL Light theories that I need
to support some verified Haskell libraries, the beginnings of which
can be found in hol-light/opentheory/examples/

However, I think it will be some time before I export any theories
that expand the HOL4 universe. My future plans include packaging up my
HOL4 probability theories, which will require the real numbers to be
packaged, and then the HOL Light complex numbers would be reachable
and interesting to HOL4 users, but that's some way off. However, your
idea of building a HOL4 exporter would certainly help with this.

Cheers,

Joe

On Thu, Jan 13, 2011 at 4:42 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> Have you exported any articles for things outside the standard
> library? Is it easy? (Anything is relatively hard for me since I don't
> have ocaml installed, but if it's easy to export any theory once I
> have hol-light installed I might consider doing it myself)
>
> I'm thinking of testing my reader on something HOL4 users would
> actually want. (I'm going to test it on more stdlib stuff first though
> probably.)
>