Def Lean.Name.decapitalize

Modification history

2024-01-01 19:29
Mathlib/Lean/Name.lean
refactor: decapitalize names in `@[mk_iff]` (#9378) …
Added Lean.Name.decapitalizeView on Github →