def Lean.Elab.Tactic.Doc.elabTacticExtension : Command.CommandElab

def Lean.Elab.Tactic.Doc.elabRegisterTacticTag : Command.CommandElab

def Lean.Elab.Tactic.Doc.elabPrintTacTags : Command.CommandElab

Displays all available tactic tags, with documentation.

structure Lean.Elab.Tactic.Doc.TacticDoc : Type

The information needed to display all documentation for a tactic.

• internalName : Name

  The name of the canonical parser for the tactic

• userName : String

  The user-facing name to display (typically the first keyword token)

• tags : NameSet

  The tags that have been applied to the tactic

• docString : Option String

  The docstring for the tactic

• extensionDocs : Array String

  Any docstring extensions that have been specified

def Lean.Elab.Tactic.Doc.allTacticDocs : MetaM (Array TacticDoc)