@@ -191,12 +191,14 @@ def mathlibLabelData : (l : Label) → LabelData l
191191 dependencies := #[.«t-ring-theory »] }
192192 | .«t-algebraic-topology » => {}
193193 | .«t-analysis » => {}
194- | .«t-category-theory » => {}
194+ | .«t-category-theory » => {
195+ dependencies := #[.«t-data »] }
195196 | .«t-combinatorics » => {}
196197 | .«t-computability » => {}
197198 | .«t-condensed » => {}
198199 | .«t-convex-geometry » => {
199- dirs := #["Mathlib" / "Geometry" / "Convex" ] }
200+ dirs := #["Mathlib" / "Geometry" / "Convex" ],
201+ dependencies := #[.«t-algebra »] }
200202 | .«t-data » => {
201203 dirs := #[
202204 "Mathlib" / "Control" ,
@@ -229,7 +231,8 @@ def mathlibLabelData : (l : Label) → LabelData l
229231 dirs := #[
230232 "Mathlib" / "MeasureTheory" ,
231233 "Mathlib" / "Probability" ,
232- "Mathlib" / "InformationTheory" ] }
234+ "Mathlib" / "InformationTheory" ]
235+ dependencies := #[.«t-analysis », .«t-algebra »] }
233236 | .«t-meta » => {
234237 dirs := #[
235238 "Mathlib" / "Lean" ,
@@ -238,11 +241,13 @@ def mathlibLabelData : (l : Label) → LabelData l
238241 "Mathlib" / "Util" ],
239242 exclusions := #["Mathlib" / "Tactic" / "Linter" ] }
240243 | .«t-number-theory » => {}
241- | .«t-order » => {}
244+ | .«t-order » => {
245+ dependencies := #[.«t-data »] }
242246 | .«t-ring-theory » => {
243247 dependencies := #[.«t-algebra », .«t-group-theory »] }
244248 | .«t-set-theory » => {}
245- | .«t-topology » => {}
249+ | .«t-topology » => {
250+ dependencies := #[.«t-order », .«t-analysis »] }
246251 | .«CI » => {
247252 dirs := #[
248253 ".github" ,
0 commit comments