Documentation

Lean.Elab.Tactic.Doc

source
def Lean.Elab.Tactic.Doc.elabTacticExtension :
Command.CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Doc.elabRegisterTacticTag :
Command.CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.Doc.elabPrintTacTags :
Command.CommandElab

Displays all available tactic tags, with documentation.

Equations
  • One or more equations did not get rendered due to their size.
source
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

source
def Lean.Elab.Tactic.Doc.allTacticDocs :
MetaM (Array TacticDoc)
Equations
  • One or more equations did not get rendered due to their size.