9 lines
177 B
Text
9 lines
177 B
Text
|
Fixpoint rec_fib (m : nat) (a : nat) (b : nat) : nat :=
|
||
|
|
match m with
|
||
|
|
| 0 => a
|
||
|
|
| S k => rec_fib k b (a + b)
|
||
|
|
end.
|
||
|
|
|
||
|
|
Definition fib (n : nat) : nat :=
|
||
|
|
rec_fib n 0 1 .
|