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

Lean.Parser.Level.paren = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "paren" (some `Lean.Parser.Level.paren)) (Lean.Parser.leadingNode `Lean.Parser.Level.paren 1024 (HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => HAndThen.hAndThen Lean.Parser.levelParser fun x => Lean.Parser.symbol ")"))

def Lean.Parser.Level.max :

Lean.Parser.Parser

Equations

Lean.Parser.Level.max = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "max" (some `Lean.Parser.Level.max)) (Lean.Parser.leadingNode `Lean.Parser.Level.max 1024 (HAndThen.hAndThen (Lean.Parser.nonReservedSymbol "max" true) fun x => Lean.Parser.many1 (HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.levelParser Lean.Parser.maxPrec)))

def Lean.Parser.Level.imax :

Lean.Parser.Parser

Equations

Lean.Parser.Level.imax = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "imax" (some `Lean.Parser.Level.imax)) (Lean.Parser.leadingNode `Lean.Parser.Level.imax 1024 (HAndThen.hAndThen (Lean.Parser.nonReservedSymbol "imax" true) fun x => Lean.Parser.many1 (HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.levelParser Lean.Parser.maxPrec)))

def Lean.Parser.Level.hole :

Lean.Parser.Parser

Equations

Lean.Parser.Level.hole = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "hole" (some `Lean.Parser.Level.hole)) (Lean.Parser.leadingNode `Lean.Parser.Level.hole 1024 (Lean.Parser.symbol "_"))

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)