coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adam AT chlipala.net>
- To: Adam Megacz <megacz AT cs.berkeley.edu>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Re: more generous context when typing branches of [match]?
- Date: Thu, 25 Mar 2010 08:35:00 -0400
And I just want to suggest the way that _I_ would write this function, which involves no proofs and no extra type annotations.
Fixpoint next (n : nat) z (t : test z) : test (z+1) -> Z :=
match n with
| 0%nat => fun _ => 3
| S n' =>
match t with
| down _ d => fun _ => next n' _ d (down _ d)
| up _ u => fun _ => 3
end
end.
If you read CPDT, you will learn the tricks you need for almost every dependently-typed function to be this easy to write. If you try to extrapolate from experience in normal functional programming, it will probably take a _lot_ of experimenting to get there.
(I can anticipate some reservations about the above code taking advantage of some aspect of the simplified function definition you gave. If this code _did_ use the function's second [test] argument in an interesting way, it really would be available with the appropriate type in the appropriate places.)
- [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
Archive powered by MhonArc 2.6.16.