Commit 2026-09-21 08:35 e85fae95

View on Github →

chore: move a few utility methods on Lean.Name to Mathlib/Lean/Name (#44007) This is a more natural location for them. Spotted while reviewing #43915.

Estimated changes

Modified Mathlib/Lean/Expr/Basic.lean

deleted def Lean.Name.fromComponents

deleted def Lean.Name.isBlackListed

deleted def Lean.Name.isPrefixOf?

deleted def Lean.Name.lastComponentAsString

deleted def Lean.Name.mapPrefix

deleted def Lean.Name.splitAt

deleted def Lean.Name.updateLast

Modified Mathlib/Lean/Name.lean

modified def Lean.Name.decapitalize

added def Lean.Name.fromComponents

added def Lean.Name.isBlackListed

added def Lean.Name.isPrefixOf?

added def Lean.Name.lastComponentAsString

added def Lean.Name.mapPrefix

added def Lean.Name.splitAt

added def Lean.Name.updateLast

Modified Mathlib/Tactic/DeprecateTo.lean

Modified Mathlib/Tactic/SetNotationForOrder.lean

Modified Mathlib/Tactic/Simps/Basic.lean

Modified Mathlib/Tactic/ToFun.lean

Modified Mathlib/Tactic/Translate/Core.lean

Modified Mathlib/Util/AliasIn.lean

Modified Mathlib/Util/PrintSorries.lean