Agda.TypeChecking.DeadCode

Documentation

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

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 - all parameter sections (because all sections go into interfaces!) (see also issues #6931 and #7382) - local builtins - all rewrite rules We only ever prune dead metavariables and definitions. The reachable ones are returned from this function.