| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.DeadCode
Synopsis
- eliminateDeadCode :: Map ModuleName a -> BuiltinThings PrimFun -> DisplayForms -> Signature -> LocalMetaStore -> TCM (DisplayForms, Signature, RemoteMetaStore)
Documentation
Arguments
| :: Map ModuleName a | Exported modules whose telescopes should not be mutilated by the dead-code removal. |
| -> BuiltinThings PrimFun | |
| -> DisplayForms | |
| -> Signature | |
| -> LocalMetaStore | |
| -> TCM (DisplayForms, Signature, RemoteMetaStore) |
Run before serialisation to remove any definitions and meta-variables that are not reachable from the module's public interface.
Things that are reachable only from warnings are removed.