Slightly higher in precedence than the logical connectives
are the LSL eq-oprs,
first-order quantifiers,
and the satisfies operator.
Informal descriptions also fit into the syntax at this level of
precedence.
equality-term ::= lsl-op-term [ eq-opr lsl-op-term ]
| quantifier [ quantifier ] ... ( term )
| higher-order-comparison
| informal-desc
eq-opr ::= = | == | \eq | ~= | != | \neq
An equality-term may have any sort, since no eq-opr need be used. See below for more details on the sorts of each form of equality-term.
See section 6.1.5 LSL Operator Terms for the syntax and meaning of lsl-op-terms. See section 6.13 Specifying Higher-Order Functions for the meaning of higher-order-comparison. See section 6.1.4 Informal Descriptions for the syntax and meaning of informal-desc. The other equality-terms are described below.
Go to the first, previous, next, last section, table of contents.