<div dir="ltr"><div>Hi Joe,<br><br></div><div>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:<br><ol><li>It proves many useful theorems as found in the basic libraries of the HOL theorem prover.<br></li><li>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.</li></ol></div><div>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.)<br><br></div><div>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?<br><br></div><div>Cheers,<br></div><div>Ramana<br></div></div>