Choose with if
Functions that decide: if, then, else, comparisons and several cases.
In this course 7 / 11
A function often has to choose. if … then … else … picks one of two results:
def shipping (express : Bool) : Nat :=
if express then 9 else 4
#eval shipping true
#eval shipping false9 4
The condition can be any true/false question: a Bool, a comparison such as n < 10 or a == b, or several combined with && (and), || (or) and ! (not).
Both branches must have the same type, because the function promises one result type whichever branch runs. For more than two cases, put another if in the else branch.
Worked example
def fee (items : Nat) : Nat :=
if items < 10 then 0 else items - 10
def size (n : Nat) : String :=
if n < 10 then "small"
else if n < 100 then "medium"
else "large"
#eval fee 4
#eval fee 25
#eval size 42size checks its conditions from the top and returns the first branch that applies.
if c then a else b chooses a result. Both branches have the same type, and nested ifs handle more cases.
Write clamp (lo n : Nat) : Nat, which returns lo when n is below lo, and n otherwise. It keeps a number from going under a lower bound.
Suggested steps
- Define clamp with two Nat parameters
- Choose with if, then, else
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:These lines run underneath whatever you write. They are what decides the exercise, so your names and types have to match them.
example : clamp 5 2 = 5 := by rfl example : clamp 5 8 = 8 := by rfl example : clamp 5 5 = 5 := by rfl
Knowledge check
Answer without looking back, then check your reasoning.
correct