The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 04/25/2014 01:45 PM, Kirill Taran wrote:

>  if you just wanted to define it or if you also wanted to use it for computing
It is better to have computable version. I see that Acc is from Wf module but didn't learn it yet,
so it would be good if you could give details.

For a detailed discussion of general recursive programming in Coq, see Chapter 7 of CPDT <http://adam.chlipala.net/cpdt/>.