Programs
Fibonacci
Turn the mathematical definition of Fibonacci numbers into a recursive program.
Open Fibonacci.lean in editordef fib : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => fib n + fib (n + 1)
def main : IO Unit := do
for i in List.range 10 do
IO.println s!"fib({i}) = {fib i}"
Explanation
Nat → Nat
A function from natural numbers to natural numbers. Type \to and accept the suggestion to insert →.
| pattern =>
Pattern matching chooses a branch based on the input.
for … in … do
Repeats an action for every element. List.range 10 contains 0 through 9.
Expected output
Reference only. Run the file to check its actual result.
fib(0) = 0 fib(1) = 1 fib(2) = 1 fib(3) = 2 fib(4) = 3 fib(5) = 5 fib(6) = 8 fib(7) = 13 fib(8) = 21 fib(9) = 34
Exercise
Print the first 12 Fibonacci numbers. This deliberately simple implementation repeats work for large inputs.