Def Lean.registerNameMapAttribute

Modification history

2022-09-04 16:26

Mathlib/Lean/NameMapAttribute.lean

feat: depend on std4 (#397)

Deleted Lean.registerNameMapAttribute View on Github →

2022-05-11 23:41

Mathlib/Lean/NameMapAttribute.lean

feat: `to_additive` (#234) …

Added Lean.registerNameMapAttribute View on Github →