The Coq mailing list

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

Hi,

Sorry, I modified my code without checking it. I indeed wanted to call 
recursively test2:

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


What is really strange for me is that the recursion is /trivially/ 
structurally decreasing.

-- 
JH

----- Mail original -----
> De: "Pierre Casteran" 
> <pierre.casteran AT labri.fr>
> À: "Jacques-Henri Jourdan" 
> <jacques-henri.jourdan AT inria.fr>
> Cc: 
> coq-club AT inria.fr
> Envoyé: Lundi 15 Juillet 2013 17:33:01
> Objet: Re: [Coq-Club] Fixpoint definition
> 
> 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
> 
> 
> 
>