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

Agda.TypeChecking.Eliminators

Synopsis

Documentation

data ElimView Source

Constructors

VarElim Nat [Elim] 
DefElim QName [Elim] 
ConElim QName [Elim] 
MetaElim MetaId [Elim] 
NoElim Term 

elimView :: Term -> TCM ElimViewSource

unElimView :: ElimView -> TermSource

Only used when producing error messages.

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