If-Then-Else

Conditional Expressions

In Lean, if/then/else is an expression (not a statement), so it always returns a value:

def max (a b : Nat) : Nat :=
  if a >= b then a else b

#eval max 10 20    -- 20
#eval max 30 5     -- 30

Both branches must have the same type.

You can nest if-then-else:

def classify (n : Nat) : String :=
  if n == 0 then "zero"
  else if n < 10 then "small"
  else "large"

Your Turn

Define a function isEven that returns true if a number is even, false otherwise.

Hint: A number is even if n % 2 == 0.