Fibonacci sequence: Difference between revisions

Content added Content deleted

Inline

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