## 2.7. `if then else`

The expression `if` `Ec` `then` `Et` `else` `Ef` is a conditional expression. It executes as follows:

• If `Ec` deflates to `true`, execute `Et`.

• If `Ec` deflates to `false`, execute `Ef`.

• If `Ec` deflates to a non-Boolean value, halt.

• If `Ec` halts silently, halt.

### 2.7.1. Syntax

 [15] Conditional `::=` `if` Expression `then` Expression `else` Expression

### 2.7.2. Type

The type of `if` `Ec` `then` `Et` `else` `Ef` is the join of the types of `Et` and `Ef`. Additionally, `Ec` must have type `Boolean`.

### 2.7.3. Examples

Binary Search in a Sorted Array
```{-
Binary search in a sorted array.
-}

def binary_search(x,a) =
def searchIn(lo, hi) =
if (lo >= hi) then
false
else (
val mid = (lo+hi) / 2
val y = a(mid)?
if (x = y) then
true
else if (x <: y) then
searchIn(lo, mid)
else
searchIn(mid+1, hi)
)
searchIn(0, a.length?)

val a = Array(15)

for(0, 15) >i>
a(i) := 2*i >>
stop ;

binary_search(19, a) | binary_search(22, a)

{-
OUTPUT:PERMUTABLE
true
false
-}
```