The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Hi coqclub,

If I define a list this way (I have some reasonnably good reason not to 
currify the constructor here):

Inductive lst :=
| Nil | Cons : nat*lst -> lst.

I can do some fixpoint computation this way :

Fixpoint test l :=
  match l with
    | Nil => 0
    | Cons (t, q) =>
      test q
  end.

However, the termination checker fails on this similar test case:

Fixpoint test2 p :=
  match p with
    | (_, Nil) => 0
    | (_, Cons l) =>
      test l
  end.

Do you have any idea why ? Is there a common workaround (other than 
using the other formulation above, that would lead to a lot of code 
duplication in my case) ?

Thanks,
--
Jacques-Henri Jourdan