The Coq mailing list

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

Vilhelm, that's it! Would the same code work in Haskell or OCaml?

Cheers,

Andrew Pennebaker

www.yellosoft.us

2011/11/3 Vilhelm Sjöberg <vilhelm AT cis.upenn.edu>

On Thu, Nov 03, 2011 at 03:12:32PM -0400, Andrew Pennebaker wrote:
> Definition one : nat := S O.
> Definition two : nat := S(S O).
>

> 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?

"one" gets interpreted as a variable bound by the match. You need to write out
the term using constructors:
 | (S O) => one

Vilhelm Sjoberg