Fibonacci sequence: Difference between revisions
Content added Content deleted
Puppydrum64 (talk | contribs) |
|||
| Line 6,687: | Line 6,687: | ||
=={{header|Lean}}== |
=={{header|Lean}}== |
||
It runs on Lean 3.4.2 |
It runs on Lean 3.4.2: |
||
<lang |
<lang Lean> |
||
-- Our first implementation is the usual recursive definition: |
-- Our first implementation is the usual recursive definition: |
||
def fib1 : ℕ → ℕ |
def fib1 : ℕ → ℕ |
||
| Line 6,709: | Line 6,709: | ||
#eval fib1 20 |
#eval fib1 20 |
||
#eval fib2 20</lang> |
#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}}== |
=={{header|LFE}}== |
||