[opentheory-users] extending the standard library

[Ramana Kumar]

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:

   1. It proves many useful theorems as found in the basic libraries of the
   HOL theorem prover.
   2. 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160410/072629ff/attachment.html>