Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Fixpoint definition

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fixpoint definition


Chronological Thread 
  • From: Pierre Casteran <pierre.casteran AT labri.fr>
  • To: Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Fixpoint definition
  • Date: Mon, 15 Jul 2013 17:33:01 +0200

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






Archive powered by MHonArc 2.6.18.

Top of Page