[opentheory-users] definition of "new" constants?

[Günter Rote]

Am 08.08.2015 um 03:16 schrieb Joe Leslie-Hurd:
> Thanks for the clarification, I have added a note to defineConst and
> defineTypeOp to spell this out:
> 
> http://www.gilith.com/research/opentheory/article.html#defineConstCommand
> http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand

Thanks. But what is the *principal* type of the new constant?
(And maybe you want to update defineConstList as well?)

Am 15.01.2011 um 03:16 schrieb Joe Leslie-Hurd:
http://www.gilith.com/opentheory/mailing-list/2011-January/000080.html
>> Also, it's not clear whether a "new constant" with the same name as
>> a previously defined constant is allowed. I presume so.
>
> This is left to the system, which must be careful to disallow
>
1. define `c = T`
2. define `c = F`
3. prove `T = F`
>
> I believe all of the HOL theorem provers maintain a symbol table of
> constants, and will not allow redefinitions with the same name. The
> logical kernel of the opentheory tool stores the definition with the
> constant, so will happily allow redefinitions with the same name
> (because the two "c" constants above will be treated as different
> constants).

This puzzles me.
If I now create another "instance" of a constant with name c
(and type bool) by a const+constTerm command, to which
constant from among definitions 1 or 2 (if any) does it
refer to? (More specifically, to which c will it be
alpha-equivalent, when this is for example tested in
the course of eqMP?)
And does the answer change for a constant c that was
"created" before definitions 1 and 2?

best regards : Günter

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5311 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150809/798762c7/attachment.bin>