The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

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