The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Greetings,

Maybe I am stupid but I really don't understand why clause in this example
is redundant:

Coq < Section Proba.

Coq < Parameter z : nat.
z is assumed

Coq <
Coq < Definition funkcija (x y : nat) : Prop :=
Coq <   match x<y with
Coq <       True => z=5
Coq <     | _    => z=10
Coq <   end.
Warning: pattern True is understood as a pattern variable
Toplevel input, characters 84-96
>     | _    => z=10
>       ^^^^^^^^^^^^
Error: This clause is redundant

To avoid this I use this function:

Fixpoint nat_lt (n m:nat) {struct n} : bool :=
  match n with
    0 => match m with
           0 => false
           | S m' => true
         end
    | S n' => match m with
                0 => false
                | S m' => nat_lt n' m'
              end
  end.

and then I match "nat_lt x y" with "true" and "| _" and then is everything
OK.
But, I don't understand why. In Reference Manual I read:

"Terms with useless patterns are not accepted by the system."

I don't see that "| _    => z=10" is "useless".

Can somebody explain me what's the point?

Thank you very much,

Marko Malikoviæ