IdrisDoc: Data.Nat.Fib

Data.Nat.Fib

Properties of the Fibonacci function.

fibAcc : Nat -> Nat -> Nat -> Nat

Accumulator for fibItr.

fibAdd : (n : Nat) -> (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> fibAcc n a b + fibAcc n c d = fibAcc n (a + c) (b + d)

Helper lemma for fibacc.

fibEq : (n : Nat) -> fibRec n = fibItr n

Iterative and recursive Fibonacci definitions are equivalent.

fibItr : Nat -> Nat

Iterative definition of Fibonacci.

fibRec : Nat -> Nat

Recursive definition of Fibonacci.

plusLemma : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> a + b + (c + d) = a + c + (b + d)

Addend shuffling lemma.