Anonymous user
Fibonacci sequence: Difference between revisions
→{{header|Lean}}
Line 5,932:
=={{header|Lean}}==
It runs on Lean 3.4.2 or later:
<lang lean>
-- Our first implementation is the usual recursive definition:
| 0 := 0▼
def fib1
| (n + 2) := fib1 n + fib1 (n + 1)
-- We can give a second more efficient implementation using an auxiliary function:
def fib_aux : ℕ → ℕ → ℕ → ℕ
def fib2 : ℕ → ℕ
-- Use #eval to do check computations:
#eval fib1 20
#eval fib2 20</lang>
| |||