@[inline]

def Lean.Parser.precedenceParser (rbp : Nat := 0) : Parser

@[inline]

def Lean.Parser.syntaxParser (rbp : Nat := 0) : Parser

def Lean.Parser.precedence : Parser

def Lean.Parser.optPrecedence : Parser

def Lean.Parser.Syntax.numPrec : Parser

def Lean.Parser.Syntax.paren : Parser

def Lean.Parser.Syntax.cat : Parser

def Lean.Parser.Syntax.unary : Parser

def Lean.Parser.Syntax.binary : Parser

def Lean.Parser.Syntax.sepBy : Parser

def Lean.Parser.Syntax.sepBy1 : Parser

def Lean.Parser.Syntax.atom : Parser

def Lean.Parser.Syntax.nonReserved : Parser

def Lean.Parser.Command.namedName : Parser

def Lean.Parser.Command.optNamedName : Parser

def Lean.Parser.Command.prefix : Parser

def Lean.Parser.Command.infix : Parser

def Lean.Parser.Command.infixl : Parser

def Lean.Parser.Command.infixr : Parser

def Lean.Parser.Command.postfix : Parser

def Lean.Parser.Command.mixfixKind : Parser

def Lean.Parser.Command.mixfix : Parser

def Lean.Parser.Command.identPrec : Parser

def Lean.Parser.Command.optKind : Parser

def Lean.Parser.Command.notationItem : Parser

def Lean.Parser.Command.notation : Parser

def Lean.Parser.Command.macro_rules : Parser

def Lean.Parser.Command.syntax : Parser

def Lean.Parser.Command.syntaxAbbrev : Parser

def Lean.Parser.Command.catBehaviorBoth : Parser

def Lean.Parser.Command.catBehaviorSymbol : Parser

def Lean.Parser.Command.catBehavior : Parser

def Lean.Parser.Command.syntaxCat : Parser

def Lean.Parser.Command.macroArg : Parser

def Lean.Parser.Command.macroRhs : Parser

def Lean.Parser.Command.macroTail : Parser

def Lean.Parser.Command.macro : Parser

def Lean.Parser.Command.elab_rules : Parser

def Lean.Parser.Command.elabArg : Parser

def Lean.Parser.Command.elabTail : Parser

def Lean.Parser.Command.elab : Parser

def Lean.Parser.Command.binderPredicate : Parser

Declares a binder predicate. For example:

binder_predicate x " > " y:term => `($x > $y)