[opentheory-users] Importing from the Gilith OpenTheory Repo

Rob Arthan rda at lemma-one.com
Mon Dec 2 17:04:21 UTC 2013


On 24 Nov 2013, at 09:45, Ramana Kumar <ramana at member.fsf.org> wrote:

> I think the idea of the base package is that everything in it should already be supported by your theorem prover, so you don't need to import it - rather, you use it as a dependency for things you export from your theorem prover.
My plan was to import the base package but using the ProofPower definitions (or theorems derived from them) rather than making new definitions so that I would end up importing all the theorems about the ProofPower constants and types that I need to support the dependencies of other packages. Isn't that what you are expected to do?

On this topic, I note that there are a number of names in the base package in the HOLLight namespace. E.g., "HOLLight.mk_pair. Is that intentional?



More information about the opentheory-users mailing list