The Coq mailing list

[Andrew Pennebaker <andrew.pennebaker AT gmail.com>]

I'm following the Software Foundations tutorial, and I decided to write a fibonacci function.

Inductive nat : Set :=

| O : nat
| S : nat -> nat.

Fixpoint plus (n m : nat) : nat :=
match n with

| O => m
| S n' => S (plus n' m)

end.

Fixpoint mult (n m : nat) : nat :=

match n with
| O => O

| S n' => plus m (mult n' m)
end.

Definition one : nat := S O.
Definition two : nat := S(S O).

Fixpoint minus (n m : nat) : nat :=
match n, m with

| O, _ => O
| S _, O => n

| S n', S m' => minus n' m'
end.

Fixpoint fib (n : nat) : nat :=
match n with

| O => O
|  one

| _ => plus (fib (minus n one)) (fib (minus n two))
end.

When I tell CoqIDE to go forward with the fib function, it reports "Error: This clause is redundant", and underlines the last case in fib:

_ => plus (fib (minus n one)) (fib (minus n two))

What am I doing wrong?

Cheers,

Andrew Pennebaker

www.yellosoft.us