Commit 2021-12-28 11:55 1fd2cbef

View on Github →

refactor: make @[ext] an attribute (on structures) (#153) Instead of a macro expansion.

Estimated changes

deleted structure Mathlib.Tactic.Ext.$n:ident