Every boolean in the Agda codebase can actually be one of True, False, or An internal error has occurred. Please report this as a bug.

@amy Wow this may be the most honest language implementation I've ever seen

@amy A type theory either has canonicity, doesn’t have canonicity, or a secret third thing

@totbwf or __IMPOSSIBLE__ called from Agda.TypeChecking.Subst

@totbwf The "you idiot, you tried to apply a Level again" error message

@amy Agda is very much like JS in this regard; we just prefer more verbose names than null and undefined

@totbwf A term can either be normal, neutral, a redex, or __IMPOSSIBLE_VERBOSE__

Sign in to participate in the conversation

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