coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Fixpoint definition, Jacques-Henri Jourdan, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Pierre Casteran, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Jacques-Henri Jourdan, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Jacques-Henri Jourdan, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Jacques-Henri Jourdan, 07/16/2013
- Re: [Coq-Club] Fixpoint definition, Jacques-Henri Jourdan, 07/16/2013
- Re: [Coq-Club] Fixpoint definition, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Daniel Schepler, 07/16/2013
- Re: [Coq-Club] Fixpoint definition, Jacques-Henri Jourdan, 07/16/2013
- Re: [Coq-Club] Fixpoint definition, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Jacques-Henri Jourdan, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Michiel Helvensteijn, 07/15/2013
- Re: [Coq-Club] Fixpoint definition, Pierre Casteran, 07/15/2013
Archive powered by MHonArc 2.6.18.