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

[Günter Rote]

> http://www.gilith.com/research/opentheory/article.html#defineConstListCommand
> 
>>> 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?
>>
>> Neither. The only way to get the constants from the definitions in 1 and 2
>> is as the objects returned by the definition commands.
> 
> Ramana has this right. And to answer your follow-up question, since
> the opentheory logical kernel is purely functional it doesn't matter
> which order definitions happen.
> 
O.K. (But it appears more like a object-oriented feature to me:
nothing is equal unless one explicitly defines it to be equal).

Two more questions:
1) If I create several constants with name c
(and the same type bool) by a sequence of const+constTerm commands,
are they equal (alpha-equivalent) to each other?
(Like "T" and "T"?)

2) If I define two constants c with the defineConst command
with the *same* definition, are they considered equal?

In any case, I think the documentation needs some clarification,
in particular here:

const
    Higher order logic constants, such as T and =.
    *Constants are identified by name*

It seems rather that the name acts merely as a comment in the above cases.
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/8872aabe/attachment.bin>