coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Reference request for detecting structurally decreasing arguments in fixpoints

From: Andrej Bauer <andrej.bauer AT andrej.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Reference request for detecting structurally decreasing arguments in fixpoints
Date: Tue, 20 Mar 2012 07:08:09 +0100

How does Coq detect a structurally decreasing argument in a fixpoint?
Is this described somewhere?

Pointers to relevant literature would be greately appreciated! (This
is about an undergraduate student project.)

With kind regards,

Andrej

[Coq-Club] Reference request for detecting structurally decreasing arguments in fixpoints, Andrej Bauer
- Re: [Coq-Club] Reference request for detecting structurally decreasing arguments in fixpoints, Stéphane Glondu