Slightly higher in precedence operators are the logical connectives.
logical-term ::= logical-term logical-opr equality-term | equality-term logical-opr ::=
The terms on either side of a logical-opr
must have sort
These also have the usual meaning;
\and mean "and",
\or mean "or",
\implies mean "implies".
See page 161 of [Guttag-Horning93] for a formal statement.
One can also use the C++ syntax
as lsl-ops (see section 6.1.5 LSL Operator Terms),
as these are defined in a Larch/C++ built-in trait.
(See section 11.4 bool for details on the trait
However, these do not have the same precedence as the
logical-oprs that are their equivalents
Go to the first, previous, next, last section, table of contents.