Agda-2.3.0: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Eliminators

Synopsis

Documentation

unElimView :: ElimView -> Term

Only used when producing error messages.

unElim :: Term -> [Elim] -> Term