**Go backward to** 2.3.4.4 Sorted Terms

**Go up to** 2.3.4 Terms

#### 2.3.4.5 Conditional Terms

CONDITIONAL ::= conditional TERM FORMULA TERM

A conditional term is written:

*T*_{1} *when* *F* *else* *T*_{2}

It is well-sorted for some sort when both *T*_{1} and *T*_{2}
are well-sorted for that sort and *F* is a well-formed formula.
The enclosing *atomic* formula
`*A*[*T*_{1} *when* *F* *else* *T*_{2}]'
expands to:

*(A[**T*_{1}] *if* *F*)
/\ (A[*T*_{2}] *if* ¬ *F*)

When several conditional terms occur in the same atomic formula, the
expansions are made in a fixed but arbitrary order (all orders yield
equivalent formulae).

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk