coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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".
|
- [Coq-Club] Question about Exhaustive Matches, Jack Kolb, 05/10/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Beta Ziliani, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Cedric Auger, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Gopalan Nadathur, 05/23/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Adam Chlipala, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Cedric Auger, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Adam Chlipala, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Cedric Auger, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Adam Chlipala, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Jason Gross, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Adam Chlipala, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Cedric Auger, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Adam Chlipala, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Beta Ziliani, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Jason Gross, 05/13/2014
- Re: [Coq-Club] Question about Exhaustive Matches, Cedric Auger, 05/13/2014
Archive powered by MHonArc 2.6.18.