Agda-2.6.4.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.DeadCode

Synopsis

Documentation

eliminateDeadCode Source #

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.