Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: more generous context when typing branches of [match]?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: more generous context when typing branches of [match]?


chronological Thread 
  • 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.)




Archive powered by MhonArc 2.6.16.

Top of Page