@[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

Declares 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

Adds 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.

def Lean.Parser.Attr.tactic_name : Parser

Sets the tactic's name.

Ordinarily, tactic names are automatically set to the first token in the tactic's parser. If this process fails, or if the tactic's name should be multiple tokens (e.g. let rec), then this attribute can be used to provide a name.

The tactic's name is used in documentation as well as in completion. Thus, the name should be a valid prefix of the tactic's syntax.

Equations

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