The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi Jacques-Henri,


> However, the termination checker fails on this similar test case:
>
> Fixpoint test2 p :=
>   match p with
>     | (_, Nil) => 0
>     | (_, Cons l) =>
>       test l
>   end.

This is not the termination checker that fails, but the type checker
Your test2 should take as argument a pair (the type of the first component is
left unspecified, but cartesian product are not recursive types.

The closest solution I think about should be:

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

Is this what you meant ?

Pierre


> 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