@[inline]

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

Equations

• Lean.Parser.precedenceParser rbp = Lean.Parser.categoryParser `prec rbp

@[inline]

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

Equations

• Lean.Parser.syntaxParser rbp = Lean.Parser.categoryParser `stx rbp

def Lean.Parser.precedence : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.optPrecedence : Lean.Parser.Parser

Equations

• Lean.Parser.optPrecedence = Lean.Parser.optional (Lean.Parser.atomic Lean.Parser.precedence)

def Lean.Parser.Syntax.numPrec : Lean.Parser.Parser

Equations

• Lean.Parser.Syntax.numPrec = Lean.Parser.checkPrec Lean.Parser.maxPrec >> Lean.Parser.numLit

def Lean.Parser.Syntax.paren : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.cat : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.unary : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.binary : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.sepBy : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.sepBy1 : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.atom : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Syntax.nonReserved : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.namedName : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.optNamedName : Lean.Parser.Parser

Equations

• Lean.Parser.Command.optNamedName = Lean.Parser.optional Lean.Parser.Command.namedName

def Lean.Parser.Command.prefix : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.infix : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.infixl : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.infixr : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.postfix : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.mixfixKind : Lean.Parser.Parser

Equations

• Lean.Parser.Command.mixfixKind = (Lean.Parser.Command.prefix <|> Lean.Parser.Command.infix <|> Lean.Parser.Command.infixl <|> Lean.Parser.Command.infixr <|> Lean.Parser.Command.postfix)

def Lean.Parser.Command.mixfix : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.identPrec : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.optKind : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.notationItem : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.notation : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.macro_rules : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.syntax : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.syntaxAbbrev : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.catBehaviorBoth : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.catBehaviorSymbol : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.catBehavior : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.syntaxCat : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.macroArg : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.macroRhs : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.macroTail : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.macro : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.elab_rules : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.elabArg : Lean.Parser.Parser

Equations

• Lean.Parser.Command.elabArg = Lean.Parser.Command.macroArg

def Lean.Parser.Command.elabTail : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.elab : Lean.Parser.Parser

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Command.binderPredicate : Lean.Parser.Parser

Declares a binder predicate. For example:

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

Equations

• One or more equations did not get rendered due to their size.