The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

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.

--
www.mhelvens.net