coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Megacz <megacz AT cs.berkeley.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Re: more generous context when typing branches of [match]?
- Date: Thu, 25 Mar 2010 19:00:13 +0000
- Cancel-lock: sha1:ufwuw7EhxhjlcZ3uXg9CdoarWTk=
- Organization: Myself
Adam Chlipala
<adam AT chlipala.net>
writes:
> The order you chose couldn't possibly work.
Hrm, could you please clarify?
Specifically, what type you believe the last occurrence of [u] has in
the program below, and how is it semantically distinct from [test (z+1)]?
Inductive test : Z -> Set :=
| up : forall z, test (z+1) -> test z
| down : forall z, test z -> test (z+1).
Fixpoint next(z:Z)(t:test z)(q:test (z+1)) : Z :=
match t with
| up _ u => next z t u
| down _ d => 3
end.
Thanks again for your comments,
- a
- [Coq-Club] more generous context when typing branches of [match]?, Adam Megacz
- Re: [Coq-Club] more generous context when typing branches of [match]?, Damien Pous
- Re: [Coq-Club] more generous context when typing branches of [match]?, Adam Chlipala
- Re: [Coq-Club] more generous context when typing branches of [match]?,
Matthew Brecknell
- [Coq-Club] Re: more generous context when typing branches of [match]?,
Adam Megacz
- Re: [Coq-Club] Re: more generous context when typing branches of [match]?,
Adam Chlipala
- Re: [Coq-Club] Re: more generous context when typing branches of [match]?, Adam Chlipala
- [Coq-Club] Re: more generous context when typing branches of [match]?,
Adam Megacz
- Re: [Coq-Club] Re: more generous context when typing branches of [match]?,
Adam Chlipala
- [Coq-Club] Re: more generous context when typing branches of [match]?, Adam Megacz
- Re: [Coq-Club] Re: more generous context when typing branches of [match]?,
Adam Chlipala
- Re: [Coq-Club] Re: more generous context when typing branches of [match]?,
Adam Chlipala
- [Coq-Club] Re: more generous context when typing branches of [match]?,
Adam Megacz
Archive powered by MhonArc 2.6.16.