Skip to content

Commit 27d395e

Browse files
committed
chore(Tactic): move StacksAttribute to CrossRefAttribute (#39257)
This PR moves StacksAttribute.lean to CrossRefAttribute.lean both in Mathlib/Tactic/ and in MathlibTest/. In the future, we can refactor the file to abstract over the type of cross-references. Currently, cross-reference attributes are implemented for the Stacks Project and Kerodon. A good candidate for a future PR is to add an attribute for Wikidata identifiers.
1 parent bcb9e00 commit 27d395e

11 files changed

Lines changed: 10 additions & 10 deletions

File tree

Mathlib.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7101,6 +7101,7 @@ public import Mathlib.Tactic.Contrapose
71017101
public import Mathlib.Tactic.Conv
71027102
public import Mathlib.Tactic.Convert
71037103
public import Mathlib.Tactic.Core
7104+
public import Mathlib.Tactic.CrossRefAttribute
71047105
public import Mathlib.Tactic.DSimpPercent
71057106
public import Mathlib.Tactic.DeclarationNames
71067107
public import Mathlib.Tactic.DefEqAbuse
@@ -7317,7 +7318,6 @@ public import Mathlib.Tactic.Simps.Basic
73177318
public import Mathlib.Tactic.Simps.NotationClass
73187319
public import Mathlib.Tactic.SplitIfs
73197320
public import Mathlib.Tactic.Spread
7320-
public import Mathlib.Tactic.StacksAttribute
73217321
public import Mathlib.Tactic.Subsingleton
73227322
public import Mathlib.Tactic.Substs
73237323
public import Mathlib.Tactic.SuccessIfFailWithMsg

Mathlib/Algebra/Ring/Defs.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@ module
77

88
public import Mathlib.Algebra.GroupWithZero.Defs
99
public import Mathlib.Data.Int.Cast.Defs
10+
public import Mathlib.Tactic.CrossRefAttribute
1011
public import Mathlib.Tactic.Spread
11-
public import Mathlib.Tactic.StacksAttribute
1212

1313
/-!
1414
# Semirings and rings

Mathlib/CategoryTheory/Category/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@ module
88
public import Mathlib.CategoryTheory.Category.Init
99
public import Mathlib.Combinatorics.Quiver.Basic
1010
public import Mathlib.Tactic.PPWithUniv
11+
public import Mathlib.Tactic.CrossRefAttribute
1112
public import Mathlib.Tactic.Common
12-
public import Mathlib.Tactic.StacksAttribute
1313
public import Mathlib.Tactic.TryThis
1414

1515
/-!

Mathlib/Tactic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,7 @@ public import Mathlib.Tactic.Contrapose
7474
public import Mathlib.Tactic.Conv
7575
public import Mathlib.Tactic.Convert
7676
public import Mathlib.Tactic.Core
77+
public import Mathlib.Tactic.CrossRefAttribute
7778
public import Mathlib.Tactic.DSimpPercent
7879
public import Mathlib.Tactic.DeclarationNames
7980
public import Mathlib.Tactic.DefEqAbuse
@@ -290,7 +291,6 @@ public import Mathlib.Tactic.Simps.Basic
290291
public import Mathlib.Tactic.Simps.NotationClass
291292
public import Mathlib.Tactic.SplitIfs
292293
public import Mathlib.Tactic.Spread
293-
public import Mathlib.Tactic.StacksAttribute
294294
public import Mathlib.Tactic.Subsingleton
295295
public import Mathlib.Tactic.Substs
296296
public import Mathlib.Tactic.SuccessIfFailWithMsg

Mathlib/Topology/Irreducible.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@ module
88
public import Mathlib.Order.Minimal
99
public import Mathlib.Order.Zorn
1010
public import Mathlib.Topology.ContinuousOn
11-
public import Mathlib.Tactic.StacksAttribute
1211
public import Mathlib.Topology.DiscreteSubset
12+
public import Mathlib.Tactic.CrossRefAttribute
1313

1414
/-!
1515
# Irreducibility in topological spaces

Mathlib/Topology/JacobsonSpace.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ module
77

88
public import Mathlib.Topology.LocalAtTarget
99
public import Mathlib.Topology.Separation.Regular
10-
public import Mathlib.Tactic.StacksAttribute
10+
public import Mathlib.Tactic.CrossRefAttribute
1111

1212
/-!
1313

Mathlib/Topology/Separation/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ public import Mathlib.Topology.Piecewise
1111
public import Mathlib.Topology.Separation.SeparatedNhds
1212
public import Mathlib.Topology.Compactness.LocallyCompact
1313
public import Mathlib.Topology.Bases
14-
public import Mathlib.Tactic.StacksAttribute
14+
public import Mathlib.Tactic.CrossRefAttribute
1515

1616
/-!
1717
# Separation properties of topological spaces

Mathlib/Topology/Separation/Regular.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@ Authors: Johannes Hölzl, Mario Carneiro
55
-/
66
module
77

8-
public import Mathlib.Tactic.StacksAttribute
98
public import Mathlib.Topology.Compactness.Lindelof
109
public import Mathlib.Topology.Separation.Hausdorff
1110
public import Mathlib.Topology.Connected.Clopen
11+
public import Mathlib.Tactic.CrossRefAttribute
1212

1313
/-!
1414
# Regular, normal, T₃, T₄ and T₅ spaces

Mathlib/Topology/Spectral/Hom.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@ Authors: Yaël Dillies
55
-/
66
module
77

8-
public import Mathlib.Tactic.StacksAttribute
98
public import Mathlib.Topology.ContinuousMap.Basic
109
public import Mathlib.Topology.Maps.Proper.Basic
10+
public import Mathlib.Tactic.CrossRefAttribute
1111

1212
/-!
1313
# Spectral maps

0 commit comments

Comments
 (0)