Ahh so that's how Agda is designed
@amy Can confirm.
@pigworker out with design by committee, in with design by Martin
@amy not exactly...but he does teach with Agda, which is worth a lot
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.