The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Adam Megacz wrote:
> 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.
>    

The previous piece of example code you sent had these two [match] cases 
swapped.