Agda-2.6.3: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.DeadCode

Synopsis

Documentation

eliminateDeadCode :: BuiltinThings PrimFun -> DisplayForms -> Signature -> LocalMetaStore -> TCM (DisplayForms, Signature, RemoteMetaStore) Source #

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.