HtDD is a recipe about inductive definitions and eliminators
@ionchy LITERALLY TRUE
@iitalics "template" "trust the natural recursion" these are just eliminators
@ionchy htdp is a big conspiracy to teach you type theory
@iitalics @ionchy It's not even a conspiracy, we keep telling the 110 students this. They don't understand, but we tell them anyway.
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.