The lowest precedence operator in a `term`
is `if then else`

.
Note that for an `if then else`

,
there must always be an `else`

part,
like the C++ operator "`?:`

".

term::=`if`

term`then`

term`else`

term|logical-term

In an `if then else`

term, the first `term`
must have sort `Bool`

, and the other terms must have the same sort,
which is the sort of the whole term.
The meaning is just what you would expect.
See page 162 of [Guttag-Horning93] for a formal statement.

Note that in LSL, there are no undefined terms;
so technically, even a term such as `div(5,0)`

would have a value.
But with the use of `if then else`

, one can ignore the
values of such terms.
For example, the following is equivalent to `x' = 3`

.

if true then x' = 3 else x' = div(5,0)

Go to the first, previous, next, last section, table of contents.