Follow
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.
@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__
@amy A type theory either has canonicity, doesn’t have canonicity, or a secret third thing