[opentheory-users] redundant import check

[Joe Leslie-Hurd]

Hi Ramana,

> In general, though, I note that it is effectively impossible to define a
> constant in OpenTheory without also proving a theorem about it.
> To get around this, I prove a trivial theorem (|- c = c) about a new
> constant c to ensure its definition is picked up.

I have thought about this limitation from time to time, but I have
never found a compelling use case for exporting symbols with no
defining properties. Can you tell me why you need to export symbols
like this?

> 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.

If you have encountered a situation where removing a redundant import
changes the resulting theory in any way (including introducing a new
error about different constants with the same name), then something is
wrong with the OpenTheory design or the implementation of it.

I don't think there is much I can do without seeing an example of this
happening, because to my mind it just shouldn't happen.

Cheers,

Joe