The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Mon, Jul 15, 2013 at 5:33 PM, Pierre Casteran
<pierre.casteran AT labri.fr>
 wrote:

> Definition  test2 (p: nat * lst) :=
>   match p with
>     | (_, Nil) => 0
>     | (_, (Cons l as l')) =>
>       test l'
>   end.
>
> Is this what you meant ?

I don't think this is what he means. I believe he meant to call
`test2` recursively. Then the function would be well-typed, but
ill-formed w.r.t. the principal argument.

(I don't have an answer yet.)

--
www.mhelvens.net