| Safe Haskell | Safe-Inferred |
|---|---|
| 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.