nothing can stop me from making extremely unfunny jokes about how the inductive-inductive version of [something] is called [something]-[something].

oh yeah the constructor-constructors. the case-case tree

@amy writing some recursive-recursive functions i see

@amy the termination-termination checker will stop you

@agdakx @amy you mean the termination-termination checker?

@agdakx Not a fan of Eliminating-eliminating higher pattern-pattern matching? 🥲

Sign in to participate in the conversation

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