Dependency atlas

The declaration-level dependency structure of this project, in two relations. Meaning edges follow statements and definition bodies: they carry what a declaration says, so an error in a definition propagates along them. Proof edges additionally follow what proofs use: they carry truth, not meaning — a statement whose proof uses a lemma does not change meaning if that lemma is wrong, but its proof breaks. Views: core ranks declarations by how much rests on them, map and module matrix show the module-level structure, and declaration focuses on one declaration's dependencies and dependents.