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?
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?