λleanlab

Fibonacci

Turn the mathematical definition of Fibonacci numbers into a recursive program.

Open Fibonacci.lean in editor
def 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.