coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>
- To: Michiel Helvensteijn <mhelvens AT gmail.com>
- Cc: Pierre Casteran <pierre.casteran AT labri.fr>, coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Fixpoint definition
- Date: Tue, 16 Jul 2013 11:22:49 +0200 (CEST)
----- 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
>
- [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.