coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?

From: Chris Dams <chris.dams.nl AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?
Date: Sat, 2 Nov 2013 07:27:14 +0100

Dear Eric,

Well, well-founded recursion is exactly what can help you define such a function. Try typing the following into coq.

Require Import Arith.
Check well_founded_induction lt_wf.

The type of "well_founded_induction lt_wf" is basically what you seem to want.

Good luck!

Chris

[Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Chris Dams, 11/02/2013
  - Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
    - Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, AUGER Cédric, 11/02/2013
      - Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
    - Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Chris Dams, 11/02/2013
      - Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Erik Silkensen, 11/02/2013
        
        Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Rui Baptista, 11/02/2013
- Re: [Coq-Club] Writing a recursive function that's not quite structurally recursive?, Adam Chlipala, 11/02/2013