The Coq mailing list

[Erik Silkensen <eriksilkensen AT gmail.com>]

Hi Chris, 

Thanks for such a quick reply and for the pointer to well_founded_induction 
lt_wf.  Does this mean I should be using the Fix tactic?  Or Function or 
Program Fixpoint?  I think I’m getting stuck on how syntactically it should 
look for this basic example.  Thanks again,

-Erik

On Nov 2, 2013, at 2:27 AM, Chris Dams 
<chris.dams.nl AT gmail.com>
 wrote:

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