Fibonacci sequence: Difference between revisions
→{{header|Lean}}
Puppydrum64 (talk | contribs) |
|||
Line 6,687:
=={{header|Lean}}==
It runs on Lean 3.4.2
<lang
-- Our first implementation is the usual recursive definition:
def fib1 : ℕ → ℕ
Line 6,709:
#eval fib1 20
#eval fib2 20</lang>
It runs on Lean 4:
<lang Lean>
-- Naive version
def fib1 (n : Nat) : Nat :=
match n with
| 0 => 0
| 1 => 1
| (k + 2) => fib1 k + fib1 (k + 1)
-- More efficient version
def fib_aux (n : Nat) (a : Nat) (b : Nat) : Nat :=
match n with
| 0 => b
| (k + 1) => fib_aux k (a + b) a
def fib2 (n : Nat) : Nat :=
fib_aux n 1 0
-- Examples
#eval fib1 20
#eval fib2 20
</lang>
=={{header|LFE}}==
| |||