Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • 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



Archive powered by MhonArc 2.6.16.

Top of Page