10 lines
259 B
Agda
10 lines
259 B
Agda
module FibonacciSequence where
|
||
|
||
open import Data.Nat using (ℕ ; zero ; suc ; _+_)
|
||
|
||
rec_fib : (m : ℕ) -> (a : ℕ) -> (b : ℕ) -> ℕ
|
||
rec_fib zero a b = a
|
||
rec_fib (suc k) a b = rec_fib k b (a + b)
|
||
|
||
fib : (n : ℕ) -> ℕ
|
||
fib n = rec_fib n zero (suc zero)
|