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

Agda.TypeChecking.DeadCode

Synopsis

Documentation

eliminateDeadCode :: ScopeInfo -> TCM (RemoteMetaStore, Definitions) Source #

Run before serialisation to remove data that's not reachable from the public interface. We do not compute reachable data precisely, because that would be very expensive, mainly because of rewrite rules. The following things are assumed to be "roots": - public names (for definitions and pattern synonyms) - definitions marked as primitive - definitions with COMPILE pragma - parameter sections of public modules - local builtins - all rewrite rules We only ever prune dead metavariables and definitions. The reachable ones are returned from this function.