The Coq mailing list

[Benjamin Werner <(e6fa90e88c%hidden_head%e6fa90e88c)ben(e6fa90e88c%hidden_at%e6fa90e88c)benjamin.werner.name(e6fa90e88c%hidden_end%e6fa90e88c)>]

Hi,

Le 16 déc. 2009 à 12:22, Andrea Poles a écrit :

Fixpoint divide (a b:nat) {struct b} : bool :=
match lwt b a with
true => false
match a with
 O => false
 match b with
   a => true
   | _ => divide a minus(b a)
   end
 end
end.

Divide should return true if b%a =0 false otherwise, but the Coqide
returns "Error: This clause is redundant." on this line:
   | _ => divide a minus(b a).

You are misunderstanding pattern-matching in the clause

a => true.

Here you want to test equality between a and b. You shoud use

a function testing equality between natural numbers. Like dec_eq_nat

defined in the library Peano_dec.

Here, the clause a => true matches all natural numbers; the fact that 

there is another variable named a is irrelevant.

This way to handle pattern-matching is not specific to Coq but shared by

most functional languages (ML, Haskell, etc).

Benjamin