coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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/>. |
- Re: [Coq-Club] external proof of termination, (continued)
- Re: [Coq-Club] external proof of termination, Jason Gross, 04/25/2014
- Re: [Coq-Club] external proof of termination, Arnaud Spiwack, 04/28/2014
- Re: [Coq-Club] external proof of termination, Eddy Westbrook, 04/25/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/25/2014
- Re: [Coq-Club] external proof of termination, Eddy Westbrook, 04/25/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/25/2014
- Re: [Coq-Club] external proof of termination, Eddy Westbrook, 04/25/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/25/2014
- Re: [Coq-Club] external proof of termination, gallais, 04/28/2014
- Re: [Coq-Club] external proof of termination, gallais, 04/28/2014
- Re: [Coq-Club] external proof of termination, Guillaume Melquiond, 04/25/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/25/2014
- Re: [Coq-Club] external proof of termination, Adam Chlipala, 04/25/2014
- Re: [Coq-Club] external proof of termination, Guillaume Melquiond, 04/25/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/26/2014
- Re: [Coq-Club] external proof of termination, Kirill Taran, 04/25/2014
- Re: [Coq-Club] external proof of termination, Jason Gross, 04/25/2014
Archive powered by MHonArc 2.6.18.