Structure Mathlib.Tactic.Ext.$n:ident

Modification history

2021-12-28 11:55
Mathlib/Tactic/Ext.lean
refactor: make @[ext] an attribute (on structures) (#153) …
Deleted Mathlib.Tactic.Ext.$n:identView on Github →
2021-10-18 09:49
Mathlib/Tactic/Ext.lean
feat: ext tactic (#73) …
Added Mathlib.Tactic.Ext.$n:identView on Github →