[opentheory-users] Importing from the Gilith OpenTheory Repo

Joe Leslie-Hurd joe at gilith.com
Tue Dec 10 21:36:03 UTC 2013

Hi Rob,

I wanted to follow up on the HOLLight namespace issue:

> > 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?
> > That is definitely not intentional, and I even have a script that
> ensures that no symbols in the HOLLight namespace escape to the standard
> theory library. I have a feeling that I have not updated the base package
> on gilith for too long, and will upload the latest version when I return
> from my vacation next week.
>  think all the names in the HOLLight namespace are related to type
> definitions. I look forward to seeing the updated base package.

I've just updated the base package


but I see that the new version also contains symbols in the HOLLight

However, the HOLLight symbol names do not appear in any exported theorem,
and so are contained within a single theory package. (This is actually what
my script checks, not that there are no HOLLight names anywhere.)

I believe this means is that these names are transient, and you can replace
them with any fresh names (perhaps using a ProofPower version of gensym?),
without changing any exported theorem in the standard theory library.

Does that resolve the issue?


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131210/08909348/attachment.html>

More information about the opentheory-users mailing list