Lean4
/-- `notation3` declares notation using Lean-3-style syntax.
Examples:
```
notation3 "∀ᶠ " (...) " in " f ", " r:(scoped p => Filter.eventually p f) => r
notation3 "MyList[" (x", "* => foldr (a b => MyList.cons a b) MyList.nil) "]" => x
```
By default notation is unable to mention any variables defined using `variable`, but
`local notation3` is able to use such local variables.
Use `notation3 (prettyPrint := false)` to keep the command from generating a pretty printer
for the notation.
This command can be used in mathlib4 but it has an uncertain future and was created primarily
for backward compatibility.
-/
@[command_parser 1000]
public meta def notation3 : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Notation3.notation3 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.unary✝ `optional (ParserDescr.const✝ `docComment))
(ParserDescr.unary✝ `optional (ParserDescr.parser✝ `Lean.Parser.Term.attributes)))
(ParserDescr.parser✝ `Lean.Parser.Term.attrKind))
(ParserDescr.symbol✝ "notation3"))
(ParserDescr.unary✝ `optional (ParserDescr.parser✝ `Lean.Parser.precedence)))
(ParserDescr.unary✝ `optional (ParserDescr.parser✝ `Lean.Parser.Command.namedName)))
(ParserDescr.unary✝ `optional (ParserDescr.parser✝ `Lean.Parser.Command.namedPrio)))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) Mathlib.Notation3.prettyPrintOpt)))
(ParserDescr.unary✝ `many1
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) Mathlib.Notation3.notation3Item)))
(ParserDescr.symbol✝ " => "))
(ParserDescr.cat✝ `term 0))
