Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Question about Exhaustive Matches

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about Exhaustive Matches


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Question about Exhaustive Matches
  • Date: Tue, 13 May 2014 10:07:59 -0400

Thanks for a good example that I hope contributes further to convincing the Coq team to remove this confusing flavor of type inference for dependent [match]. :)  I don't think there is a simple explanation of the behavior you see, and IMO it would be better to require a [return] annotation on every [match] (that isn't at the top level of a definition) giving the dependent typing scheme explicitly.

On 05/10/2014 04:29 PM, Jack Kolb wrote:
In this case, I get the helpful error message: "Non exhaustive pattern-matching: no clause found for pattern 1." However, something strange happens when I make a similar mistake in the second of the two definitions given above:

Definition nat_ind3: forall (P : nat -> Prop),
  P 0 -> P 1 -> P 2 ->
  (forall n : nat, P n -> P (S (S (S n)))) ->
  forall n : nat, P n :=
    fun P => fun P0 => fun P1 => fun P2 => fun PSSS =>
      fix f (n:nat) := match n with
         0 => P0
       | 1 => P1
       | (S (S (S n'))) => PSSS n' (f n')
     end.

In this case, I get the following error message:

In environment
P : nat -> Prop
P0 : P 0
P1 : P 1
P2 : P 2
PSSS : forall n : nat, P n -> P (S (S (S n)))
f : nat -> P 0
n : nat
n0 : nat
The term "P1" has type "P 1" while it is expected to have type "P 0".





Archive powered by MHonArc 2.6.18.

Top of Page