Def Mathlib.Notation3.MatchState.getBinders

Modification history

2023-08-26 12:33

Mathlib/Mathport/Notation.lean

feat: multiple `scoped` in `notation3` (#6793) …

Added Mathlib.Notation3.MatchState.getBinders View on Github →