Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Created looping combinator.
In order to get rid of the grey link in view of all the material we have on coinduction, I made coinductive definition a stub that redirects to definition and coinduction.
I intentionally did not do that, because our page coinduction is about proof by coinduction.
I see that you created inductive definition to go along with it. I would suggest that instead, inductive definition should redirect to inductive type and similarly for coinductive definition (although coinductive type remains to be written).
Okay, I made inductive definition point to inducive type for the precise definition.
I hope you don’t mean that there is harm done by the entry coinductive definition. It needs to be fleshed out, but the single sentence currently there is still better than a broken link, I’d think.
Well, I think the statement “a coinductive definition is a definition by coinduction” is not correct, or at least misleading, given that our page coinduction uses the word to refer only to proofs about a structure that has already been coinductively defined. But I’m not asking you to fix it; maybe I’ll get around to writing coinductive type one of these days.
1 to 6 of 6