@[inline]

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

Equations

• Lean.Parser.priorityParser rbp = Lean.Parser.categoryParser `prio rbp

@[inline]

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

Equations

• Lean.Parser.attrParser rbp = Lean.Parser.categoryParser `attr rbp

def Lean.Parser.Priority.numPrio : Parser

Equations

• Lean.Parser.Priority.numPrio = Lean.Parser.checkPrec Lean.Parser.maxPrec >> Lean.Parser.numLit

def Lean.Parser.Attr.simple : Parser

Equations

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

def Lean.Parser.Attr.macro : Parser

Equations

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

def Lean.Parser.Attr.export : Parser

Equations

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

def Lean.Parser.Attr.recursor : Parser

Equations

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

def Lean.Parser.Attr.class : Parser

Equations

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

def Lean.Parser.Attr.instance : Parser

Equations

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

def Lean.Parser.Attr.default_instance : Parser

Equations

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

def Lean.Parser.Attr.specialize : Parser

Equations

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

def Lean.Parser.Attr.externEntry : Parser

Equations

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

def Lean.Parser.Attr.extern : Parser

Equations

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

def Lean.Parser.Attr.tactic_alt : Parser

Declare this tactic to be an alias or alternative form of an existing tactic.

This has the following effects:

• The alias relationship is saved
• The docstring is taken from the original tactic, if present

Equations

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

def Lean.Parser.Attr.tactic_tag : Parser

Add one or more tags to a tactic.

Tags should be applied to the canonical names for tactics.

Equations

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