Documentation

Lean.Parser.Level

@[inline]

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

Lean.Parser.Parser

Equations

Lean.Parser.levelParser rbp = Lean.Parser.categoryParser `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

Lean.Parser.Level.addLit = Lean.Parser.trailingNode `Lean.Parser.Level.addLit 65 0 (HAndThen.hAndThen (Lean.Parser.symbol " + ") fun x => Lean.Parser.numLit)