Term equality

Uses Logical truth

Syntactic equality of terms (are the terms displayed identically?) can be tested with:
 s:𝕊, s == s : 𝔹

Term equality is symmetric:
 s_:𝕊, x:s_, y:s_, (x == y) = (y == x)

The actual evaluation of equality can only be implemented outside of Leibniz:
 s_:𝕊, x:s_, y:s_, x == y ⇒ Pharo:"x isSyntacticallyEqualTo: y"

Examples:
 ⊤ == ⊤ ⇒ ⊤
 ⊤ == ⊥ ⇒ ⊥
 ⊥ == ⊥ ⇒ ⊤