You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

jsalvatier comments on No coinductive datatype of integers - Less Wrong Discussion

4 Post author: cousin_it 04 May 2011 04:37PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (138)

You are viewing a single comment's thread.

Comment author: jsalvatier 04 May 2011 06:36:01PM *  2 points [-]

This seems like a decent place to ask: I'm slowly trying to learn Type Theory. I haven't seen a place where (Co)Inductive datatypes (as in the Calculus of (Co)Inductive Constructions) are explained formally (though preferably for novice readers); does anyone have a a suggestion?