2.15.4 Conditional expressions

A conditional expression is an expression of either of the two following forms

(if Goal then Expression1 else Expression2)
(Goal -> Expression1 ; Expression2)

Goal is a goal; Expression1 and Expression2 are both data-terms. The semantics of a conditional expression is that if Goal is true, then the expression has the meaning of Expression1, else the expression has the meaning of Expression2.

If Goal takes the form some [X, Y, Z] … then the scope of X, Y, and Z includes Expression1.