Commit 2024-07-10 10:57 cf79f2ed

View on Github →

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.

Estimated changes

deleted theorem UFModel.Agrees.empty
deleted theorem UFModel.Agrees.get_eq'
deleted theorem UFModel.Agrees.get_eq
deleted theorem UFModel.Agrees.mk'
deleted theorem UFModel.Agrees.push
deleted theorem UFModel.Agrees.set
deleted theorem UFModel.Agrees.size_eq
deleted inductive UFModel.Agrees
deleted theorem UFModel.Models.empty
deleted theorem UFModel.Models.parent_eq'
deleted theorem UFModel.Models.parent_eq
deleted theorem UFModel.Models.push
deleted theorem UFModel.Models.rank_eq
deleted theorem UFModel.Models.setParent
deleted theorem UFModel.Models.size_eq
deleted def UFModel.Models
deleted def UFModel.empty
deleted def UFModel.push
deleted def UFModel.setParent
deleted structure UFModel
deleted structure UFNode
deleted def UnionFind.empty
deleted def UnionFind.find
deleted def UnionFind.findAux
deleted def UnionFind.link
deleted theorem UnionFind.lt_rankMax'
deleted theorem UnionFind.lt_rankMax
deleted def UnionFind.mkEmpty
deleted theorem UnionFind.model'
deleted theorem UnionFind.parent_lt
deleted def UnionFind.push
deleted def UnionFind.rank
deleted def UnionFind.rankMax
deleted theorem UnionFind.rank_eq
deleted theorem UnionFind.rank_lt
deleted def UnionFind.size
deleted def UnionFind.union
deleted structure UnionFind