<div dir="ltr"><div><div><div><div><div><div><div>Hi Joe,<br><br></div>Thanks for the clarification. I think you interpreted my question correctly.<br></div>After reading your description, I think the checks for redundant imports in a theory block are correct as is.<br><br></div><div>In general, though, I note that it is effectively impossible to define a constant in OpenTheory without also proving a theorem about it.<br></div><div>To get around this, I prove a trivial theorem (|- c = c) about a new constant c to ensure its definition is picked up.<br></div><br></div>My original question was motivated by a problem that I still have. Namely, I receive unexpected warnings about 2 different constants with the same name. I thought this was because I hadn't imported the block that defines the constant into all the blocks that use it, but (hopefully I checked this right) if I add any of those import lines they are flagged as redundant. The warning about different constants therefore looks like a red herring; the resulting theory package doesn't appear to have any problems like unexpected axioms or assumptions or ungrounded constants.<br><br></div>Perhaps you could explain further the circumstances under which the 2 different constants warning occurs. I can also provide the relevant articles and theory packages but they are quite large and unwieldy so I'd rather hold off on that at first.<br><br></div>Cheers,<br></div>Ramana<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 31 March 2016 at 18:18, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Ramana,<br>
<br>
There are a couple of different redundant warnings the tool can<br>
generate: I assume your question is about the "redundant import X in<br>
theory block Y" warning message, not the "redundant requires: X"<br>
warning.<br>
<br>
I've just looked at the code, and for an import X to be reported as<br>
redundant in theory block Y both of the following must hold:<br>
<br>
1. The theorems of X and the assumptions of Y are disjoint.<br>
2. The defined symbols in the theorems of X and the input symbols in<br>
theorems of Y are disjoint.<br>
<br>
If I interpret your question correctly, you are concerned about<br>
removing a redundant import X containing a defined symbol S that is<br>
used in Y but not exported in a theorem. After scratching my head for<br>
some time I cannot see how removing X from the imports of Y could<br>
result in the creation of different symbols with the same name, but<br>
perhaps I am missing something.<br>
<br>
Do you have a problem scenario in mind?<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div><div class="h5"><br>
<br>
On Tue, Mar 29, 2016 at 3:03 PM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote:<br>
> Hi Joe,<br>
><br>
> I have not had time to investigate this thoroughly yet, but I have a<br>
> suspicion that the redundant import check might not check for constants that<br>
> don't appear in any theorems. Therefore, removing a "redundant" import might<br>
> result in two different constants with the same name. Do you think this is<br>
> possible?<br>
><br>
> Cheers,<br>
> Ramana<br>
><br>
</div></div>> _______________________________________________<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" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
<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" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</blockquote></div><br></div>