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

Safe Haskell | None
Language | Haskell2010

Agda.Compiler.Treeless.Erase

Synopsis

- eraseTerms :: QName -> EvaluationStrategy -> TTerm -> TCM TTerm
- computeErasedConstructorArgs :: QName -> TCM ()

# Documentation

eraseTerms :: QName -> EvaluationStrategy -> TTerm -> TCM TTerm Source #

computeErasedConstructorArgs :: QName -> TCM () Source #

Takes the name of the data/record type.