问在TLA+中是否有xor (专属或) infix操作符？

EN

假设A \in BOOLEAN /\ B \in BOOLEAN，在命题逻辑中称为"XOR“的是不等式：

A # B

它在相同的假设下相当于~ (A <=> B)。当A, B采用非布尔值时，这两个公式不一定等价.下面的公理可以描述操作符<=>

THEOREM
    ASSUME
        /\ A \in BOOLEAN
        /\ B \in BOOLEAN
    PROVE
        (A <=> B)  =  (A = B)

对于A和B的非布尔值，不指定A <=> B的值.在对布尔运算符的适度解释中，未指定A <=> B是非布尔值、A还是B的非布尔值。在布尔运算符的自由解释中，\A A, B: (A <=> B) \in BOOLEAN，如TLA版本2:初步指南中所描述的。

还请参见第10页(该页为参数的布尔值定义布尔运算符)和Sec。TLA+书的16.1.3。公式

(A \/ B) /\ ~ (A /\ B)

对于标识符A和B的非布尔值(TLA+为非类型化)也是有意义的。所以

(15 \/ "a") /\ ~ (15 /\ "a")

是一个可能的价值。我不知道TLA+是否指定此公式是否具有与

15 # "a"

另见关于附录A，第201页，实用TLA+第10行的评论。