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

Safe Haskell | Safe-Infered

Agda.TypeChecking.Eliminators

Synopsis

- data ElimView
  - = VarElim Nat [Elim]
  - | DefElim QName [Elim]
  - | ConElim QName [Elim]
  - | MetaElim MetaId [Elim]
  - | NoElim Term
- elimView :: Term -> TCM ElimView
- unElimView :: ElimView -> Term
- unElim :: Term -> [Elim] -> Term

# Documentation

data ElimView

Constructors

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

elimView :: Term -> TCM ElimView

unElimView :: ElimView -> Term

Only used when producing error messages.

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