A.2.6 Let ExpressionsA.2 ValuesA.2.4 Quantified FormulasA.2.5 Conditional Expressions

A.2.5 Conditional Expressions

Synopsis

IF E THEN E1 ELSE E2 ENDIF
IF E THEN E1
   ELSIF E' THEN E1' ... ELSE E2 ENDIF

Description

The expression IF E THEN E1 ELSE E2 ENDIF consists of a value E of type BOOLEAN and of two values E1 and E2 of same type which is also the type of the conditional expression. The value of the expression is E1, if E is TRUE, and E2, otherwise.

The more general form

IF E THEN E1
ELSIF E' THEN E1'
ELSIF E" THEN E1"
...
ELSE E2
ENDIF

is a syntactic short cut for

IF E THEN E1
ElSE IF E' THEN E1'
ELSE IF E" THEN E1"
...
ELSE E2
ENDIF ... ENDIF ENDIF


Wolfgang Schreiner

A.2.6 Let ExpressionsA.2 ValuesA.2.4 Quantified FormulasA.2.5 Conditional Expressions