Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] external proof of termination

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] external proof of termination


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] external proof of termination
  • Date: Fri, 25 Apr 2014 14:06:38 -0400

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



Archive powered by MHonArc 2.6.18.

Top of Page