@[inline]

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

Equations

• Lean.Parser.priorityParser rbp = Lean.Parser.categoryParser (Lean.Name.mkStr1 "prio") rbp

@[inline]

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

Equations

• Lean.Parser.attrParser rbp = Lean.Parser.categoryParser (Lean.Name.mkStr1 "attr") rbp

def Lean.Parser.Priority.numPrio : Lean.Parser.Parser

Equations

• Lean.Parser.Priority.numPrio = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun x => Lean.Parser.numLit

def Lean.Parser.Attr.simple : Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.macro : Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.export : Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.recursor : Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.class : Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.instance : Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.defaultInstance : Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.specialize : Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.externEntry : Lean.Parser.Parser

Equations

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

def Lean.Parser.Attr.extern : Lean.Parser.Parser

Equations

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