The Coq mailing list

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

----- Mail original -----
> De: "Michiel Helvensteijn" 
> <mhelvens AT gmail.com>
> À: "Jacques-Henri Jourdan" 
> <jacques-henri.jourdan AT inria.fr>
> Cc: "Pierre Casteran" 
> <pierre.casteran AT labri.fr>,
>  "coq-club" 
> <coq-club AT inria.fr>
> Envoyé: Lundi 15 Juillet 2013 22:37:22
> Objet: Re: [Coq-Club] Fixpoint definition
> 
> On Mon, Jul 15, 2013 at 10:16 PM, Jacques-Henri Jourdan
> <jacques-henri.jourdan AT inria.fr>
>  wrote:
> 
> >> But it's structurally decreasing through both `lst` and `pair`,
> >> and
> >> basic `Fixpoint` only understands *really trivial* structural
> >> decreasing arguments.
> >
> > Well, but it does works when it is through pair then lst, but not
> > through lst then pair, which is really confusing.
> 
> As I understand it, your first example works because it structurally
> decreases on a `lst` parameter. A `lst` can "contain itself" by
> definition.
> 
> Your second example tries to decrease on a `pair`. As far as the type
> `pair` is concerned, the actual parameter is not structurally smaller
> than the formal parameter, it's just different.

Well, I don't really see why that does make any difference, actually. This is 
a subterm, so I whould be able to recurse on it.


> 
> --
> www.mhelvens.net
>