<div dir="ltr">Hi Rob,<div><br></div><div>I've given this some thought, because this redefinition problem can occur in a number of ways. As we have just seen on the other thread</div><div><br></div><div><a href="http://www.gilith.com/opentheory/mailing-list/2014-March/000373.html">http://www.gilith.com/opentheory/mailing-list/2014-March/000373.html</a></div>
<div><br></div><div>it is not constrained to a single article file, but also occurs when importing a sequence of articles that define symbols for "internal" use.</div><div><br></div><div>What would you think of the following scheme, which involves a change to the article standard?</div>
<div><br></div><div>Declare a particular name to be special (e.g., "" or "_") for definition commands, such that when a symbol of this name is defined a reader may substitute a fresh name instead. Then when articles are generated by the opentheory tool it can check which symbols appear in exported theories, and squash all the others to "". This would allow readers with global symbol tables to read articles with internal definitions with no problems.</div>
<div><br></div><div>Thoughts?</div><div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div><div><div class="gmail_extra"><div class="gmail_quote">On Wed, Mar 19, 2014 at 7:55 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:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word">Joe,<div><br><div><div class="">
<div>On 18 Mar 2014, at 17:49, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote:</div><br><blockquote type="cite"><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></blockquote><div><br></div></div>Thanks for that, it may come in useful. It will only work if the repeated definitions all give alpha-equivalent defining properties.</div><div><br></div><div>I think the article format definition should specify whether redefinition is allowed (and I would vote strongly for a constraint forbidding redefinition).</div>
<div><br></div></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br></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></div></div>