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

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

def Lean.Elab.Tactic.Doc.firstTacticTokens {m : Type → Type} [Monad m] [MonadEnv m] : m (NameMap String)

Computes a table that heuristically maps parser syntax kinds to their first tokens by inspecting the Pratt parsing tables for the `tactic syntax kind. If a custom name is provided for the tactic, then it is returned instead.

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 (includeUnnamed : Bool := true) : MetaM (Array TacticDoc)