Commit 2024-05-14 09:16 96941f1a

View on Github →

chore: rename Name.getString -> Name.lastComponentAsString (#12891)

Estimated changes

Modified Mathlib/Lean/Expr/Basic.lean

deleted def Lean.Name.getString

added def Lean.Name.lastComponentAsString

Modified Mathlib/Tactic/Simps/Basic.lean

Modified Mathlib/Tactic/ToAdditive.lean