Slightly higher in precedence operators are the logical connectives.
logical-term ::= logical-term logical-opr equality-term
| equality-term
logical-opr ::= \and | \or | \implies | /\ | \/ | =>
The terms on either side of a logical-opr
must have sort Bool.
These also have the usual meaning;
that is, /\ and \and mean "and",
\/ and \or mean "or",
and => and \implies mean "implies".
See page 161 of [Guttag-Horning93] for a formal statement.
One can also use the C++ syntax && and ||
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 bool_sugars.)
However, these do not have the same precedence as the
logical-oprs that are their equivalents /\ and \/.
Go to the first, previous, next, last section, table of contents.