| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Compiler.MAlonzo.Coerce
Synopsis
- addCoercions :: HasConstInfo m => TTerm -> m TTerm
- erasedArity :: HasConstInfo m => QName -> m Nat
Documentation
addCoercions :: HasConstInfo m => TTerm -> m TTerm Source #
Insert unsafeCoerce (in the form of TCoerce) everywhere it's needed in
the right-hand side of a definition.
erasedArity :: HasConstInfo m => QName -> m Nat Source #
The number of retained arguments after erasure.