Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


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





Archive powered by MhonArc 2.6.16.

Top of Page