coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Beta Ziliani <beta AT mpi-sws.org>
- To: Nuno Gaspar <nmpgaspar AT gmail.com>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] should typecheck... right
- Date: Thu, 1 Aug 2013 18:18:12 +0200
Simple. Both x_nil and x_not_nil have different types. Those types, indeed, live in Prop, but that's a different story. So you're fixpoint is returning things from different types.
On Thu, Aug 1, 2013 at 6:05 PM, Nuno Gaspar <nmpgaspar AT gmail.com> wrote:
I imagine you can guess my doubt.. So why doesn't it typecheck? They both live in Prop... -_-Here follows:Hello.Well, I'm having an hard time reproducing an example I was given. I think I can resume it to the following (I'm actually not sure my simplification didn't break the original problem...but heh)
Parameter l : list nat.
Parameter x_nil : forall n:nat, In n nil.
Parameter x_not_nil : forall (n:nat), In n l.
Fixpoint test l :=
match l with
nil => x_nil
| cons e r => x_not_nil
end.How would go for making this typecheck? I'm sure it can be done..
Thank you fellas.
--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.
- [Coq-Club] should typecheck... right, Nuno Gaspar, 08/01/2013
- Re: [Coq-Club] should typecheck... right, Beta Ziliani, 08/01/2013
- Re: [Coq-Club] should typecheck... right, Valentin Robert, 08/01/2013
- Re: [Coq-Club] should typecheck... right, Cedric Auger, 08/01/2013
- Re: [Coq-Club] should typecheck... right, Nuno Gaspar, 08/01/2013
- Re: [Coq-Club] should typecheck... right, Cedric Auger, 08/01/2013
- Re: [Coq-Club] should typecheck... right, Nuno Gaspar, 08/01/2013
- Re: [Coq-Club] should typecheck... right, t x, 08/02/2013
- Re: [Coq-Club] should typecheck... right, Nuno Gaspar, 08/02/2013
- Re: [Coq-Club] should typecheck... right, t x, 08/02/2013
- Re: [Coq-Club] should typecheck... right, Nuno Gaspar, 08/01/2013
- Re: [Coq-Club] should typecheck... right, Cedric Auger, 08/04/2013
- Re: [Coq-Club] should typecheck... right, Nuno Gaspar, 08/05/2013
- Re: [Coq-Club] should typecheck... right, Cedric Auger, 08/01/2013
- Re: [Coq-Club] should typecheck... right, Nuno Gaspar, 08/01/2013
Archive powered by MHonArc 2.6.18.