[opentheory-users] article format wording about constants

[Joe Hurd]

Hi Ramana,

> This confuses me... Are you saying it's possible to have two different constant
> terms where the constants have the same name but different types, where one of
> the types is not just an instance of the other?

A trivial example of this is

[] : bool list

and

[] : num list

If these were input constants, the processing tool would never know
that they were both instances of a more general

[] : 'a list

defined in another theory.

With defined constants this should never be the case (though
theoretically a system could permit same-name constants at disjoint
types and remain sound - this was the topic of a long discussion on
the HOL4 mailing list some years back).

Cheers,

Joe