Def Mathlib.Tactic.Ext.extAttribute

Modification history

2022-09-08 18:38
Mathlib/Tactic/Ext.lean
chore: bump std4 09-08 (#403) …
Deleted Mathlib.Tactic.Ext.extAttributeView on Github →
2021-12-28 11:55
Mathlib/Tactic/Ext.lean
refactor: make @[ext] an attribute (on structures) (#153) …
Added Mathlib.Tactic.Ext.extAttributeView on Github →