Skip to content

Commit cf79f2e

Browse files
committed
chore: remove Data/UnionFind (#14556)
Its implementation has been improved in `lean4lean` and `batteries`; the mathlib implementation can be removed in favour of these. Searching github for 'import Mathlib.Data.UnionFind' only yields forks of mathlib (either explicit or manual); hence this seems safe to remove without a deprecation period.
1 parent 7bc13f8 commit cf79f2e

File tree

4 files changed

+0
-324
lines changed

4 files changed

+0
-324
lines changed

Mathlib.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2419,7 +2419,6 @@ import Mathlib.Data.TypeMax
24192419
import Mathlib.Data.TypeVec
24202420
import Mathlib.Data.UInt
24212421
import Mathlib.Data.ULift
2422-
import Mathlib.Data.UnionFind
24232422
import Mathlib.Data.Vector.Basic
24242423
import Mathlib.Data.Vector.Defs
24252424
import Mathlib.Data.Vector.MapLemmas

Mathlib/Data/UnionFind.lean

Lines changed: 0 additions & 296 deletions
This file was deleted.

scripts/nolints.json

Lines changed: 0 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -26,9 +26,6 @@
2626
["docBlame", "RightDistributive"],
2727
["docBlame", "RightIdentity"],
2828
["docBlame", "RightInverse"],
29-
["docBlame", "UFModel"],
30-
["docBlame", "UFNode"],
31-
["docBlame", "UnionFind"],
3229
["docBlame", "Writer"],
3330
["docBlame", "WriterT"],
3431
["docBlame", "Xor'"],
@@ -393,31 +390,8 @@
393390
["docBlame", "Traversable.mapFold"],
394391
["docBlame", "Tree.unitRecOn"],
395392
["docBlame", "Trivialization.baseSet"],
396-
["docBlame", "UFModel.Agrees"],
397-
["docBlame", "UFModel.Models"],
398-
["docBlame", "UFModel.empty"],
399-
["docBlame", "UFModel.parent"],
400-
["docBlame", "UFModel.push"],
401-
["docBlame", "UFModel.rank"],
402-
["docBlame", "UFModel.setParent"],
403-
["docBlame", "UFModel.setParentBump"],
404-
["docBlame", "UFNode.parent"],
405-
["docBlame", "UFNode.rank"],
406-
["docBlame", "UFNode.value"],
407393
["docBlame", "ULiftable.congr"],
408394
["docBlame", "UniformFun.phi"],
409-
["docBlame", "UnionFind.arr"],
410-
["docBlame", "UnionFind.empty"],
411-
["docBlame", "UnionFind.find"],
412-
["docBlame", "UnionFind.findAux"],
413-
["docBlame", "UnionFind.link"],
414-
["docBlame", "UnionFind.mkEmpty"],
415-
["docBlame", "UnionFind.push"],
416-
["docBlame", "UnionFind.rank"],
417-
["docBlame", "UnionFind.rankMax"],
418-
["docBlame", "UnionFind.rankMaxAux"],
419-
["docBlame", "UnionFind.size"],
420-
["docBlame", "UnionFind.union"],
421395
["docBlame", "UnivLE.witness"],
422396
["docBlame", "Valued.v"],
423397
["docBlame", "Vector3.unexpandCons"],

scripts/style-exceptions.txt

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@ Mathlib/Data/BinaryHeap.lean : line 7 : ERR_MOD : Module docstring missing, or t
22
Mathlib/Data/ByteArray.lean : line 7 : ERR_MOD : Module docstring missing, or too late
33
Mathlib/Data/QPF/Multivariate/Basic.lean : line 75 : ERR_LIN : Line has more than 100 characters
44
Mathlib/Data/String/Lemmas.lean : line 10 : ERR_MOD : Module docstring missing, or too late
5-
Mathlib/Data/UnionFind.lean : line 9 : ERR_MOD : Module docstring missing, or too late
65
Mathlib/Init/Data/Int/Basic.lean : line 11 : ERR_MOD : Module docstring missing, or too late
76
Mathlib/Init/Data/Nat/Basic.lean : line 10 : ERR_MOD : Module docstring missing, or too late
87
Mathlib/Init/Data/Nat/Lemmas.lean : line 13 : ERR_MOD : Module docstring missing, or too late

0 commit comments

Comments
 (0)