Def Lean.Name.decapitalize

Modification history

2026-09-21 08:35
Mathlib/Lean/Name.lean
chore: move a few utility methods on Lean.Name to Mathlib/Lean/Name (#44007) …
Modified Lean.Name.decapitalizeView on Github →
2024-01-01 19:29
Mathlib/Lean/Name.lean
refactor: decapitalize names in `@[mk_iff]` (#9378) …
Added Lean.Name.decapitalizeView on Github →