Documentation

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. This was originally due to rewrite rules, though this may no longer be true after support for --rewriting was dropped in Mikan.

The following things are assumed to be "roots": - public definitions - definitions marked as primitive - definitions with COMPILE pragma - all pattern synonyms (because currently all of them go into interfaces) - all parameter sections (because currently all of them go into interfaces) (see also issues #6931 and #7382) - local builtins - closed display forms We only ever prune dead metavariables and definitions. We return the pruned metas, pruned definitions and closed display forms.