EXISTL-EQUATION ::= existl-equation TERM TERM
STRONG-EQUATION ::= strong-equation TERM TERM
An existential equation EXISTL-EQUATION is written:
T1 =e= T2The sign displayed as an `e' over a `=' in LaTeX is input as `=e='.
A strong equation is written:
T1 = T2
An existential equation holds when the values of the terms are both defined and equal; a strong equation holds also when the values of both terms are undefined (thus the two forms of equation are equivalent when the values of both terms are always defined).
An equation is well-sorted if there is a sort such that both terms are well-sorted for that sort. It then expands to the corresponding existential or strong equation on the fully-qualified expansions of the terms for that sort.