Inductive Mathlib.Notation3.BoundValueType

Modification history

2023-06-02 12:48
Mathlib/Mathport/Notation.lean
feat: `notation3` delaborator generation (#4533) …
Added Mathlib.Notation3.BoundValueTypeView on Github →