Def Mathlib.Notation3.MatchState.pushBinder

Modification history

2023-08-26 12:33
Mathlib/Mathport/Notation.lean
feat: multiple `scoped` in `notation3` (#6793) …
Deleted Mathlib.Notation3.MatchState.pushBinderView on Github →
2023-06-02 12:48
Mathlib/Mathport/Notation.lean
feat: `notation3` delaborator generation (#4533) …
Added Mathlib.Notation3.MatchState.pushBinderView on Github →