[opentheory-users] Importing from the Gilith OpenTheory Repo

[Joe Leslie-Hurd]

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

http://opentheory.gilith.com/?pkg=base

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

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?

Cheers,

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