Def Lean.Name.lastComponentAsString

Modification history

2024-05-14 09:16

Mathlib/Lean/Expr/Basic.lean

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

Added Lean.Name.lastComponentAsString View on Github →