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

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.