@[inline]

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

Equations

• Lean.Parser.levelParser rbp = Lean.Parser.categoryParser (Lean.Name.mkStr1 "level") rbp

def Lean.Parser.Level.paren : Lean.Parser.Parser

Equations

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

def Lean.Parser.Level.max : Lean.Parser.Parser

Equations

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

def Lean.Parser.Level.imax : Lean.Parser.Parser

Equations

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

def Lean.Parser.Level.hole : Lean.Parser.Parser

Equations

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

def Lean.Parser.Level.num : Lean.Parser.Parser

Equations

• Lean.Parser.Level.num = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun x => Lean.Parser.numLit

def Lean.Parser.Level.ident : Lean.Parser.Parser

Equations

• Lean.Parser.Level.ident = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun x => Lean.Parser.ident

def Lean.Parser.Level.addLit : Lean.Parser.TrailingParser

Equations

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