coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Question about Exhaustive Matches
- Date: Tue, 13 May 2014 16:27:59 +0200
I think that non-dependent matches (where the type of every branch is unifiable), at least, shouldn't require [return] annotations. I also think that there should be some type inference in the return annotation; I want to be able to leave underscores for things that don't depend on the variables bound in [as] and [in].
-Jason
On Tue, May 13, 2014 at 4:23 PM, Beta Ziliani <beta AT mpi-sws.org> wrote:
On Tue, May 13, 2014 at 4:07 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:+1
> 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.
I also think cleverness can sometimes obfuscate instead of help.
>
> 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, 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, 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.