On Sun, Feb 24, 2013 at 7:47 PM, Roman Cheplyaka <roma@ro-che.info> wrote:

Or perhaps you meant that the production itself, when interpreted as a
definition, is corecursive?

I was merely thrown off by your mention of "well-founded" and the assertion that you're left with a "strictly smaller" input. I don't see any of this.

That's when I remembered that well-founded recursion (a desirable) is sometimes confused with productive corecursion (another desirable).

-- Kim-Ee