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

Equations

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

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

Equations

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

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

Displays all available tactic tags, with documentation.

Equations

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

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

The information needed to display all documentation for a tactic.

• internalName : Lake.Name

  The name of the canonical parser for the tactic

• userName : String

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

• tags : Lean.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 : Lean.MetaM (Array Lean.Elab.Tactic.Doc.TacticDoc)

Equations

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