Agda-2.8.0: 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 ()
- isErasable :: QName -> TCM Bool

# Documentation

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

computeErasedConstructorArgs :: QName -> TCM () Source #

Takes the name of the data/record type.

isErasable :: QName -> TCM Bool Source #