coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Fixpoint definition

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: Mon, 15 Jul 2013 22:16:13 +0200 (CEST)

>
> 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.

--
JH

[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, Daniel Schepler, 07/16/2013
        
        Re: [Coq-Club] Fixpoint definition, Jacques-Henri Jourdan, 07/16/2013