@[inline]

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

Equations

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

@[inline]

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

Equations

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

def Lean.Parser.precedence : Parser

Equations

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

def Lean.Parser.optPrecedence : Parser

Equations

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

def Lean.Parser.Syntax.numPrec : Parser

Equations

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

def Lean.Parser.Syntax.paren : Parser

Equations

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

def Lean.Parser.Syntax.cat : Parser

Equations

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

def Lean.Parser.Syntax.unary : Parser

Equations

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

def Lean.Parser.Syntax.binary : Parser

Equations

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

def Lean.Parser.Syntax.sepBy : Parser

Equations

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

def Lean.Parser.Syntax.sepBy1 : Parser

Equations

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

def Lean.Parser.Syntax.atom : Parser

Equations

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

def Lean.Parser.Syntax.nonReserved : Parser

Equations

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

def Lean.Parser.Command.namedName : Parser

Equations

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

def Lean.Parser.Command.optNamedName : Parser

Equations

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

def Lean.Parser.Command.prefix : Parser

Equations

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

def Lean.Parser.Command.infix : Parser

Equations

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

def Lean.Parser.Command.infixl : Parser

Equations

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

def Lean.Parser.Command.infixr : Parser

Equations

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

def Lean.Parser.Command.postfix : Parser

Equations

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

def Lean.Parser.Command.mixfixKind : 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 : Parser

Equations

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

def Lean.Parser.Command.identPrec : Parser

Equations

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

def Lean.Parser.Command.optKind : Parser

Equations

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

def Lean.Parser.Command.notationItem : Parser

Equations

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

def Lean.Parser.Command.notation : Parser

Equations

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

def Lean.Parser.Command.macro_rules : Parser

Equations

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

def Lean.Parser.Command.syntax : Parser

Equations

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

def Lean.Parser.Command.syntaxAbbrev : Parser

Equations

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

def Lean.Parser.Command.catBehaviorBoth : Parser

Equations

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

def Lean.Parser.Command.catBehaviorSymbol : Parser

Equations

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

def Lean.Parser.Command.catBehavior : Parser

Equations

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

def Lean.Parser.Command.syntaxCat : Parser

Equations

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

def Lean.Parser.Command.macroArg : Parser

Equations

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

def Lean.Parser.Command.macroRhs : Parser

Equations

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

def Lean.Parser.Command.macroTail : Parser

Equations

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

def Lean.Parser.Command.macro : Parser

Equations

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

def Lean.Parser.Command.elab_rules : Parser

Equations

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

def Lean.Parser.Command.elabArg : Parser

Equations

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

def Lean.Parser.Command.elabTail : Parser

Equations

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

def Lean.Parser.Command.elab : Parser

Equations

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

def Lean.Parser.Command.binderPredicate : 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.