Lean4
/-- `forbiddenImportDirs` relates module prefixes, specifying that modules with the first prefix
should not import modules with the second prefix (except if specifically allowed in
`overrideAllowedImportDirs`).
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 forbiddenImportDirs : NamePrefixRel :=
.ofArray
#[(`Mathlib.Algebra.Notation, `Mathlib.Algebra), (`Mathlib, `Mathlib.Deprecated),
-- This is used to test the linter.
(`MathlibTest.Header, `Mathlib.Deprecated),
-- TODO:
-- (`Mathlib.Data, `Mathlib.Dynamics),
-- (`Mathlib.Topology, `Mathlib.Algebra),
-- The following are a list of existing non-dependent top-level directory pairs.
(`Mathlib.Algebra, `Mathlib.AlgebraicGeometry), (`Mathlib.Algebra, `Mathlib.Analysis),
(`Mathlib.Algebra, `Mathlib.Computability), (`Mathlib.Algebra, `Mathlib.Condensed),
(`Mathlib.Algebra, `Mathlib.Geometry), (`Mathlib.Algebra, `Mathlib.InformationTheory),
(`Mathlib.Algebra, `Mathlib.ModelTheory), (`Mathlib.Algebra, `Mathlib.RepresentationTheory),
(`Mathlib.Algebra, `Mathlib.Testing), (`Mathlib.AlgebraicGeometry, `Mathlib.AlgebraicTopology),
(`Mathlib.AlgebraicGeometry, `Mathlib.Analysis), (`Mathlib.AlgebraicGeometry, `Mathlib.Computability),
(`Mathlib.AlgebraicGeometry, `Mathlib.Condensed), (`Mathlib.AlgebraicGeometry, `Mathlib.InformationTheory),
(`Mathlib.AlgebraicGeometry, `Mathlib.MeasureTheory), (`Mathlib.AlgebraicGeometry, `Mathlib.ModelTheory),
(`Mathlib.AlgebraicGeometry, `Mathlib.Probability), (`Mathlib.AlgebraicGeometry, `Mathlib.RepresentationTheory),
(`Mathlib.AlgebraicGeometry, `Mathlib.Testing), (`Mathlib.AlgebraicTopology, `Mathlib.AlgebraicGeometry),
(`Mathlib.AlgebraicTopology, `Mathlib.Computability), (`Mathlib.AlgebraicTopology, `Mathlib.Condensed),
(`Mathlib.AlgebraicTopology, `Mathlib.FieldTheory), (`Mathlib.AlgebraicTopology, `Mathlib.Geometry),
(`Mathlib.AlgebraicTopology, `Mathlib.InformationTheory), (`Mathlib.AlgebraicTopology, `Mathlib.MeasureTheory),
(`Mathlib.AlgebraicTopology, `Mathlib.ModelTheory), (`Mathlib.AlgebraicTopology, `Mathlib.NumberTheory),
(`Mathlib.AlgebraicTopology, `Mathlib.Probability), (`Mathlib.AlgebraicTopology, `Mathlib.RepresentationTheory),
(`Mathlib.AlgebraicTopology, `Mathlib.SetTheory), (`Mathlib.AlgebraicTopology, `Mathlib.Testing),
(`Mathlib.Analysis, `Mathlib.AlgebraicGeometry), (`Mathlib.Analysis, `Mathlib.AlgebraicTopology),
(`Mathlib.Analysis, `Mathlib.Computability), (`Mathlib.Analysis, `Mathlib.Condensed),
(`Mathlib.Analysis, `Mathlib.InformationTheory), (`Mathlib.Analysis, `Mathlib.ModelTheory),
(`Mathlib.Analysis, `Mathlib.RepresentationTheory), (`Mathlib.Analysis, `Mathlib.Testing),
(`Mathlib.CategoryTheory, `Mathlib.AlgebraicGeometry), (`Mathlib.CategoryTheory, `Mathlib.Analysis),
(`Mathlib.CategoryTheory, `Mathlib.Computability), (`Mathlib.CategoryTheory, `Mathlib.Condensed),
(`Mathlib.CategoryTheory, `Mathlib.Geometry), (`Mathlib.CategoryTheory, `Mathlib.InformationTheory),
(`Mathlib.CategoryTheory, `Mathlib.MeasureTheory), (`Mathlib.CategoryTheory, `Mathlib.ModelTheory),
(`Mathlib.CategoryTheory, `Mathlib.Probability), (`Mathlib.CategoryTheory, `Mathlib.RepresentationTheory),
(`Mathlib.CategoryTheory, `Mathlib.Testing), (`Mathlib.Combinatorics, `Mathlib.AlgebraicGeometry),
(`Mathlib.Combinatorics, `Mathlib.AlgebraicTopology), (`Mathlib.Combinatorics, `Mathlib.Computability),
(`Mathlib.Combinatorics, `Mathlib.Condensed), (`Mathlib.Combinatorics, `Mathlib.Geometry.Euclidean),
(`Mathlib.Combinatorics, `Mathlib.Geometry.Group), (`Mathlib.Combinatorics, `Mathlib.Geometry.Manifold),
(`Mathlib.Combinatorics, `Mathlib.Geometry.RingedSpace), (`Mathlib.Combinatorics, `Mathlib.InformationTheory),
(`Mathlib.Combinatorics, `Mathlib.MeasureTheory), (`Mathlib.Combinatorics, `Mathlib.ModelTheory),
(`Mathlib.Combinatorics, `Mathlib.Probability), (`Mathlib.Combinatorics, `Mathlib.RepresentationTheory),
(`Mathlib.Combinatorics, `Mathlib.Testing), (`Mathlib.Computability, `Mathlib.AlgebraicGeometry),
(`Mathlib.Computability, `Mathlib.AlgebraicTopology), (`Mathlib.Computability, `Mathlib.CategoryTheory),
(`Mathlib.Computability, `Mathlib.Condensed), (`Mathlib.Computability, `Mathlib.FieldTheory),
(`Mathlib.Computability, `Mathlib.Geometry), (`Mathlib.Computability, `Mathlib.InformationTheory),
(`Mathlib.Computability, `Mathlib.MeasureTheory), (`Mathlib.Computability, `Mathlib.ModelTheory),
(`Mathlib.Computability, `Mathlib.Probability), (`Mathlib.Computability, `Mathlib.RepresentationTheory),
(`Mathlib.Computability, `Mathlib.Testing), (`Mathlib.Condensed, `Mathlib.AlgebraicGeometry),
(`Mathlib.Condensed, `Mathlib.AlgebraicTopology), (`Mathlib.Condensed, `Mathlib.Computability),
(`Mathlib.Condensed, `Mathlib.FieldTheory), (`Mathlib.Condensed, `Mathlib.Geometry),
(`Mathlib.Condensed, `Mathlib.InformationTheory), (`Mathlib.Condensed, `Mathlib.MeasureTheory),
(`Mathlib.Condensed, `Mathlib.ModelTheory), (`Mathlib.Condensed, `Mathlib.Probability),
(`Mathlib.Condensed, `Mathlib.RepresentationTheory), (`Mathlib.Condensed, `Mathlib.Testing),
(`Mathlib.Control, `Mathlib.AlgebraicGeometry), (`Mathlib.Control, `Mathlib.AlgebraicTopology),
(`Mathlib.Control, `Mathlib.Analysis), (`Mathlib.Control, `Mathlib.Computability),
(`Mathlib.Control, `Mathlib.Condensed), (`Mathlib.Control, `Mathlib.FieldTheory),
(`Mathlib.Control, `Mathlib.Geometry), (`Mathlib.Control, `Mathlib.GroupTheory),
(`Mathlib.Control, `Mathlib.InformationTheory), (`Mathlib.Control, `Mathlib.LinearAlgebra),
(`Mathlib.Control, `Mathlib.MeasureTheory), (`Mathlib.Control, `Mathlib.ModelTheory),
(`Mathlib.Control, `Mathlib.NumberTheory), (`Mathlib.Control, `Mathlib.Probability),
(`Mathlib.Control, `Mathlib.RepresentationTheory), (`Mathlib.Control, `Mathlib.RingTheory),
(`Mathlib.Control, `Mathlib.SetTheory), (`Mathlib.Control, `Mathlib.Testing),
(`Mathlib.Control, `Mathlib.Topology), (`Mathlib.Data, `Mathlib.AlgebraicGeometry),
(`Mathlib.Data, `Mathlib.AlgebraicTopology), (`Mathlib.Data, `Mathlib.Analysis),
(`Mathlib.Data, `Mathlib.Computability), (`Mathlib.Data, `Mathlib.Condensed),
(`Mathlib.Data, `Mathlib.FieldTheory), (`Mathlib.Data, `Mathlib.Geometry.Euclidean),
(`Mathlib.Data, `Mathlib.Geometry.Group), (`Mathlib.Data, `Mathlib.Geometry.Manifold),
(`Mathlib.Data, `Mathlib.Geometry.RingedSpace), (`Mathlib.Data, `Mathlib.InformationTheory),
(`Mathlib.Data, `Mathlib.ModelTheory), (`Mathlib.Data, `Mathlib.RepresentationTheory),
(`Mathlib.Data, `Mathlib.Testing), (`Mathlib.Dynamics, `Mathlib.AlgebraicGeometry),
(`Mathlib.Dynamics, `Mathlib.AlgebraicTopology), (`Mathlib.Dynamics, `Mathlib.CategoryTheory),
(`Mathlib.Dynamics, `Mathlib.Computability), (`Mathlib.Dynamics, `Mathlib.Condensed),
(`Mathlib.Dynamics, `Mathlib.Geometry.Euclidean), (`Mathlib.Dynamics, `Mathlib.Geometry.Group),
(`Mathlib.Dynamics, `Mathlib.Geometry.Manifold), (`Mathlib.Dynamics, `Mathlib.Geometry.RingedSpace),
(`Mathlib.Dynamics, `Mathlib.InformationTheory), (`Mathlib.Dynamics, `Mathlib.ModelTheory),
(`Mathlib.Dynamics, `Mathlib.RepresentationTheory), (`Mathlib.Dynamics, `Mathlib.Testing),
(`Mathlib.FieldTheory, `Mathlib.AlgebraicGeometry), (`Mathlib.FieldTheory, `Mathlib.AlgebraicTopology),
(`Mathlib.FieldTheory, `Mathlib.Condensed), (`Mathlib.FieldTheory, `Mathlib.Geometry),
(`Mathlib.FieldTheory, `Mathlib.InformationTheory), (`Mathlib.FieldTheory, `Mathlib.MeasureTheory),
(`Mathlib.FieldTheory, `Mathlib.Probability), (`Mathlib.FieldTheory, `Mathlib.RepresentationTheory),
(`Mathlib.FieldTheory, `Mathlib.Testing), (`Mathlib.Geometry, `Mathlib.AlgebraicGeometry),
(`Mathlib.Geometry, `Mathlib.Computability), (`Mathlib.Geometry, `Mathlib.Condensed),
(`Mathlib.Geometry, `Mathlib.InformationTheory), (`Mathlib.Geometry, `Mathlib.ModelTheory),
(`Mathlib.Geometry, `Mathlib.RepresentationTheory), (`Mathlib.Geometry, `Mathlib.Testing),
(`Mathlib.GroupTheory, `Mathlib.AlgebraicGeometry), (`Mathlib.GroupTheory, `Mathlib.AlgebraicTopology),
(`Mathlib.GroupTheory, `Mathlib.Analysis), (`Mathlib.GroupTheory, `Mathlib.Computability),
(`Mathlib.GroupTheory, `Mathlib.Condensed), (`Mathlib.GroupTheory, `Mathlib.Geometry),
(`Mathlib.GroupTheory, `Mathlib.InformationTheory), (`Mathlib.GroupTheory, `Mathlib.MeasureTheory),
(`Mathlib.GroupTheory, `Mathlib.ModelTheory), (`Mathlib.GroupTheory, `Mathlib.Probability),
(`Mathlib.GroupTheory, `Mathlib.RepresentationTheory), (`Mathlib.GroupTheory, `Mathlib.Testing),
(`Mathlib.GroupTheory, `Mathlib.Topology), (`Mathlib.InformationTheory, `Mathlib.AlgebraicGeometry),
(`Mathlib.InformationTheory, `Mathlib.AlgebraicTopology), (`Mathlib.InformationTheory, `Mathlib.CategoryTheory),
(`Mathlib.InformationTheory, `Mathlib.Computability), (`Mathlib.InformationTheory, `Mathlib.Condensed),
(`Mathlib.InformationTheory, `Mathlib.Geometry.Euclidean), (`Mathlib.InformationTheory, `Mathlib.Geometry.Group),
(`Mathlib.InformationTheory, `Mathlib.Geometry.Manifold),
(`Mathlib.InformationTheory, `Mathlib.Geometry.RingedSpace), (`Mathlib.InformationTheory, `Mathlib.ModelTheory),
(`Mathlib.InformationTheory, `Mathlib.RepresentationTheory), (`Mathlib.InformationTheory, `Mathlib.Testing),
(`Mathlib.LinearAlgebra, `Mathlib.AlgebraicGeometry), (`Mathlib.LinearAlgebra, `Mathlib.AlgebraicTopology),
(`Mathlib.LinearAlgebra, `Mathlib.Computability), (`Mathlib.LinearAlgebra, `Mathlib.Condensed),
(`Mathlib.LinearAlgebra, `Mathlib.Geometry.Euclidean), (`Mathlib.LinearAlgebra, `Mathlib.Geometry.Group),
(`Mathlib.LinearAlgebra, `Mathlib.Geometry.Manifold), (`Mathlib.LinearAlgebra, `Mathlib.Geometry.RingedSpace),
(`Mathlib.LinearAlgebra, `Mathlib.InformationTheory), (`Mathlib.LinearAlgebra, `Mathlib.MeasureTheory),
(`Mathlib.LinearAlgebra, `Mathlib.ModelTheory), (`Mathlib.LinearAlgebra, `Mathlib.Probability),
(`Mathlib.LinearAlgebra, `Mathlib.Testing), (`Mathlib.LinearAlgebra, `Mathlib.Topology),
(`Mathlib.MeasureTheory, `Mathlib.AlgebraicGeometry), (`Mathlib.MeasureTheory, `Mathlib.AlgebraicTopology),
(`Mathlib.MeasureTheory, `Mathlib.Computability), (`Mathlib.MeasureTheory, `Mathlib.Condensed),
(`Mathlib.MeasureTheory, `Mathlib.Geometry.Euclidean), (`Mathlib.MeasureTheory, `Mathlib.Geometry.Group),
(`Mathlib.MeasureTheory, `Mathlib.Geometry.Manifold), (`Mathlib.MeasureTheory, `Mathlib.Geometry.RingedSpace),
(`Mathlib.MeasureTheory, `Mathlib.InformationTheory), (`Mathlib.MeasureTheory, `Mathlib.ModelTheory),
(`Mathlib.MeasureTheory, `Mathlib.RepresentationTheory), (`Mathlib.MeasureTheory, `Mathlib.Testing),
(`Mathlib.ModelTheory, `Mathlib.AlgebraicGeometry), (`Mathlib.ModelTheory, `Mathlib.AlgebraicTopology),
(`Mathlib.ModelTheory, `Mathlib.Analysis), (`Mathlib.ModelTheory, `Mathlib.Condensed),
(`Mathlib.ModelTheory, `Mathlib.Geometry), (`Mathlib.ModelTheory, `Mathlib.InformationTheory),
(`Mathlib.ModelTheory, `Mathlib.MeasureTheory), (`Mathlib.ModelTheory, `Mathlib.Probability),
(`Mathlib.ModelTheory, `Mathlib.RepresentationTheory), (`Mathlib.ModelTheory, `Mathlib.Testing),
(`Mathlib.ModelTheory, `Mathlib.Topology), (`Mathlib.NumberTheory, `Mathlib.AlgebraicGeometry),
(`Mathlib.NumberTheory, `Mathlib.AlgebraicTopology), (`Mathlib.NumberTheory, `Mathlib.Computability),
(`Mathlib.NumberTheory, `Mathlib.Condensed), (`Mathlib.NumberTheory, `Mathlib.InformationTheory),
(`Mathlib.NumberTheory, `Mathlib.ModelTheory), (`Mathlib.NumberTheory, `Mathlib.RepresentationTheory),
(`Mathlib.NumberTheory, `Mathlib.Testing), (`Mathlib.Order, `Mathlib.AlgebraicGeometry),
(`Mathlib.Order, `Mathlib.AlgebraicTopology), (`Mathlib.Order, `Mathlib.Computability),
(`Mathlib.Order, `Mathlib.Condensed), (`Mathlib.Order, `Mathlib.FieldTheory), (`Mathlib.Order, `Mathlib.Geometry),
(`Mathlib.Order, `Mathlib.InformationTheory), (`Mathlib.Order, `Mathlib.MeasureTheory),
(`Mathlib.Order, `Mathlib.ModelTheory), (`Mathlib.Order, `Mathlib.NumberTheory),
(`Mathlib.Order, `Mathlib.Probability), (`Mathlib.Order, `Mathlib.RepresentationTheory),
(`Mathlib.Order, `Mathlib.Testing), (`Mathlib.Probability, `Mathlib.AlgebraicGeometry),
(`Mathlib.Probability, `Mathlib.AlgebraicTopology), (`Mathlib.Probability, `Mathlib.CategoryTheory),
(`Mathlib.Probability, `Mathlib.Computability), (`Mathlib.Probability, `Mathlib.Condensed),
(`Mathlib.Probability, `Mathlib.Geometry.Euclidean), (`Mathlib.Probability, `Mathlib.Geometry.Group),
(`Mathlib.Probability, `Mathlib.Geometry.Manifold), (`Mathlib.Probability, `Mathlib.Geometry.RingedSpace),
(`Mathlib.Probability, `Mathlib.InformationTheory), (`Mathlib.Probability, `Mathlib.ModelTheory),
(`Mathlib.Probability, `Mathlib.RepresentationTheory), (`Mathlib.Probability, `Mathlib.Testing),
(`Mathlib.RepresentationTheory, `Mathlib.AlgebraicGeometry), (`Mathlib.RepresentationTheory, `Mathlib.Analysis),
(`Mathlib.RepresentationTheory, `Mathlib.Computability), (`Mathlib.RepresentationTheory, `Mathlib.Condensed),
(`Mathlib.RepresentationTheory, `Mathlib.Geometry), (`Mathlib.RepresentationTheory, `Mathlib.InformationTheory),
(`Mathlib.RepresentationTheory, `Mathlib.MeasureTheory), (`Mathlib.RepresentationTheory, `Mathlib.ModelTheory),
(`Mathlib.RepresentationTheory, `Mathlib.Probability), (`Mathlib.RepresentationTheory, `Mathlib.Testing),
(`Mathlib.RepresentationTheory, `Mathlib.Topology), (`Mathlib.RingTheory, `Mathlib.AlgebraicGeometry),
(`Mathlib.RingTheory, `Mathlib.AlgebraicTopology), (`Mathlib.RingTheory, `Mathlib.Computability),
(`Mathlib.RingTheory, `Mathlib.Condensed), (`Mathlib.RingTheory, `Mathlib.Geometry.Euclidean),
(`Mathlib.RingTheory, `Mathlib.Geometry.Group), (`Mathlib.RingTheory, `Mathlib.Geometry.Manifold),
(`Mathlib.RingTheory, `Mathlib.Geometry.RingedSpace), (`Mathlib.RingTheory, `Mathlib.InformationTheory),
(`Mathlib.RingTheory, `Mathlib.ModelTheory), (`Mathlib.RingTheory, `Mathlib.RepresentationTheory),
(`Mathlib.RingTheory, `Mathlib.Testing), (`Mathlib.SetTheory, `Mathlib.AlgebraicGeometry),
(`Mathlib.SetTheory, `Mathlib.AlgebraicTopology), (`Mathlib.SetTheory, `Mathlib.Analysis),
(`Mathlib.SetTheory, `Mathlib.CategoryTheory), (`Mathlib.SetTheory, `Mathlib.Combinatorics),
(`Mathlib.SetTheory, `Mathlib.Computability), (`Mathlib.SetTheory, `Mathlib.Condensed),
(`Mathlib.SetTheory, `Mathlib.FieldTheory), (`Mathlib.SetTheory, `Mathlib.Geometry),
(`Mathlib.SetTheory, `Mathlib.InformationTheory), (`Mathlib.SetTheory, `Mathlib.MeasureTheory),
(`Mathlib.SetTheory, `Mathlib.ModelTheory), (`Mathlib.SetTheory, `Mathlib.Probability),
(`Mathlib.SetTheory, `Mathlib.RepresentationTheory), (`Mathlib.SetTheory, `Mathlib.Testing),
(`Mathlib.Topology, `Mathlib.AlgebraicGeometry), (`Mathlib.Topology, `Mathlib.Computability),
(`Mathlib.Topology, `Mathlib.Condensed), (`Mathlib.Topology, `Mathlib.Geometry),
(`Mathlib.Topology, `Mathlib.InformationTheory), (`Mathlib.Topology, `Mathlib.ModelTheory),
(`Mathlib.Topology, `Mathlib.Probability), (`Mathlib.Topology, `Mathlib.RepresentationTheory),
(`Mathlib.Topology, `Mathlib.Testing), ]
