@[inline]

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

Equations

• Lean.Parser.levelParser rbp = Lean.Parser.categoryParser `level rbp

def Lean.Parser.Level.paren : Parser

Equations

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

def Lean.Parser.Level.max : Parser

Equations

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

def Lean.Parser.Level.imax : Parser

Equations

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

def Lean.Parser.Level.hole : Parser

Equations

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

def Lean.Parser.Level.num : Parser

Equations

• Lean.Parser.Level.num = Lean.Parser.checkPrec Lean.Parser.maxPrec >> Lean.Parser.numLit

def Lean.Parser.Level.ident : Parser

Equations

• Lean.Parser.Level.ident = Lean.Parser.checkPrec Lean.Parser.maxPrec >> Lean.Parser.ident

def Lean.Parser.Level.addLit : TrailingParser

Equations

• Lean.Parser.Level.addLit = Lean.Parser.trailingNode `Lean.Parser.Level.addLit 65 0 (Lean.Parser.symbol " + " >> Lean.Parser.numLit)