[opentheory-users] redundant import check

[Joe Leslie-Hurd]

Hi Ramana,

There are a couple of different redundant warnings the tool can
generate: I assume your question is about the "redundant import X in
theory block Y" warning message, not the "redundant requires: X"
warning.

I've just looked at the code, and for an import X to be reported as
redundant in theory block Y both of the following must hold:

1. The theorems of X and the assumptions of Y are disjoint.
2. The defined symbols in the theorems of X and the input symbols in
theorems of Y are disjoint.

If I interpret your question correctly, you are concerned about
removing a redundant import X containing a defined symbol S that is
used in Y but not exported in a theorem. After scratching my head for
some time I cannot see how removing X from the imports of Y could
result in the creation of different symbols with the same name, but
perhaps I am missing something.

Do you have a problem scenario in mind?

Cheers,

Joe


On Tue, Mar 29, 2016 at 3:03 PM, Ramana Kumar <ramana at member.fsf.org> wrote:
> Hi Joe,
>
> I have not had time to investigate this thoroughly yet, but I have a
> suspicion that the redundant import check might not check for constants that
> don't appear in any theorems. Therefore, removing a "redundant" import might
> result in two different constants with the same name. Do you think this is
> possible?
>
> Cheers,
> Ramana
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>