The Coq mailing list

["Harley D. Eades III" <harley.eades AT gmail.com>]

Hi, Adam.

On Dec 14, 2012, at 10:41 AM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:

> On 12/14/2012 10:33 AM, Harley D. Eades III wrote:
>> A while ago I formalized some of my research on the hereditary substitution
>> function in Coq.  At first I tried to define the function in Set using 
>> Program Fixpoint
>> and the wf annotation.  I was able to define the function and satisfy all 
>> the obligations.
>> However, I can't compute with it.  Even worse the subgoals generated are 
>> huge.  They
>> are over 1000 lines long.
>>   
> 
> Chapter 7 of CPDT <http://adam.chlipala.net/cpdt/> may be of interest.  It 
> surveys a variety of techniques for general recursion in Coq (not including 
> Program, which I've never gotten into, partly because of the issues you 
> mention).
Thanks for a lot for your feedback.

I take a look at Chap. 7.

Harley