[opentheory-users] extending the standard library

[Joe Leslie-Hurd]

Hi Ramana,

The intent is for the standard theory library to always be evolving,
but slowly, because it's supposed to contain the base theories that
*every* HOL theorem prover supports.

Looking through the theory I see a lot of defined constants that also
occur in the OpenTheory standard library (e.g., list.UNZIP), and I was
wondering why the HOL4 base theory has its own version?

Cheers,

Joe

On Sun, Apr 10, 2016 at 1:54 PM, Ramana Kumar <ramana at member.fsf.org> wrote:
> Hi Joe,
>
> You will have seen that the HOL developers have uploaded a package called
> hol-base to the Gilith repo. The purpose of this package is twofold:
>
> It proves many useful theorems as found in the basic libraries of the HOL
> theorem prover.
> It serves to satisfy the assumptions of further theories developed in the
> HOL theorem prover, by proving those assumptions using only the theorems of
> the OpenTheory standard library base package.
>
> For purpose 1 in particular, it seems to me that many of the constants
> defined by hol-base would benefit from residing in an appropriate place in
> OpenTheory's namespace hierarchy, and indeed some of the proofs from
> hol-base might beneficially be moved into the base package itself.
> (Currently, all constants defined by hol-base are in their own namespace.)
>
> Is the design of the standard library still evolving, and is it open to
> extension? Would you be willing to copy over any useful-looking constants?
> And/or settle on some namespace decisions?
>
> Cheers,
> Ramana
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>