cur icon indicating copy to clipboard operation
cur copied to clipboard

Published 20 hours ago • verified publisher icon wilbowma

Fixpoint functions

Open wilbowma opened this issue 8 years ago • 0 comments

My understanding is that Coq's Fixpoint is just a complicated macro. This paper, http://www.chargueraud.org/research/2009/fixwf/fixwf.pdf, suggests is should be simple to implement.

See if we can implement this in Cur, in terms of eliminators.

wilbowma avatar Mar 30 '16 17:03 wilbowma