HtDD is a recipe about inductive definitions and eliminators

@iitalics "template" "trust the natural recursion" these are just eliminators

@iitalics @ionchy It's not even a conspiracy, we keep telling the 110 students this. They don't understand, but we tell them anyway.

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.