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