@[inline]

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

@[inline]

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

def Lean.Parser.Priority.numPrio : Parser

def Lean.Parser.Attr.simple : Parser

def Lean.Parser.Attr.macro : Parser

def Lean.Parser.Attr.export : Parser

def Lean.Parser.Attr.recursor : Parser

def Lean.Parser.Attr.class : Parser

def Lean.Parser.Attr.instance : Parser

def Lean.Parser.Attr.default_instance : Parser

def Lean.Parser.Attr.specialize : Parser

def Lean.Parser.Attr.externEntry : Parser

def Lean.Parser.Attr.extern : Parser

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

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.

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.