Foundations · 7 min
Functions
The declaration def double (n : Nat) : Nat := n * 2 describes a function. The parentheses bind an input named n, the next colon gives the output type, and the final expression computes the result.
Lean uses spaces for function application. double 21 applies the function to 21. Parentheses are for grouping: double (3 + 4).
Exercise
Implement triple so that it multiplies its natural-number input by three.
Open exercise in editordef triple (n : Nat) : Nat :=
n
#eval triple 14
Hint
The body can be n * 3. You do not need a return keyword.
Solution
def triple (n : Nat) : Nat :=
n * 3
#eval triple 14