<div dir="ltr">Hi Rob,<div><br></div><div>The HOLLight.* symbols are "auxiliary" type operators and constants that are used in proofs but not exported by any theory. So it's not unreasonable that it is defined multiple times in subtheories of base. However, what is surprising is that the article compression algorithm implemented in the opentheory tool does not fold the multiple definitions into a single definition.</div>
<div><br></div><div>Thanks for the report: I'll look into the problem. This code will need reworking anyway to process the new article commands.</div><div><br></div><div>If the multiple definitions are causing problems then as a workaround you can pick an arbitrary new name for any symbols in the HOLLight namespace, because such symbols are guaranteed never to be appear in any exported theorem.</div>
<div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div> </div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Mar 18, 2014 at 7:56 AM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">I just installed the latest version of the base package and did:<div><br></div><div>   opentheory info —article —output base.art base</div>
<div><br></div><div>The resulting article file contains multiple definitions of various constants in the HOLLight namespace.</div><div>E.g., HOLLight.NUMSUM.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div>
</div><br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>