Lean4
/-- `overrideAllowedImportDirs` relates module prefixes, specifying that modules with the first
prefix are allowed to import modules with the second prefix, even if disallowed in
`forbiddenImportDirs`.
For example, ``(`Mathlib.Algebra.Notation, `Mathlib.Algebra)`` is in `forbiddenImportDirs` and
``(`Mathlib.Algebra.Notation, `Mathlib.Algebra.Notation)`` is in `overrideAllowedImportDirs`
because modules in `Mathlib/Algebra/Notation.lean` cannot import modules in `Mathlib.Algebra` that are
outside `Mathlib/Algebra/Notation.lean`.
-/
def overrideAllowedImportDirs : NamePrefixRel :=
.ofArray
#[(`Mathlib.Algebra.Lie, `Mathlib.RepresentationTheory), (`Mathlib.Algebra.Module.ZLattice, `Mathlib.Analysis),
(`Mathlib.Algebra.Notation, `Mathlib.Algebra.Notation), (`Mathlib.Deprecated, `Mathlib.Deprecated),
(`Mathlib.LinearAlgebra.Complex, `Mathlib.Topology), -- Complex numbers are analysis/topology.
(`Mathlib.LinearAlgebra.Matrix, `Mathlib.Topology), -- For e.g. spectra.
(`Mathlib.LinearAlgebra.QuadraticForm, `Mathlib.Topology), -- For real/complex quadratic forms.
(`Mathlib.Topology.Algebra, `Mathlib.Algebra), (`Mathlib.Topology.Compactification, `Mathlib.Geometry.Manifold)]
