def Lean.Parser.Tactic.Doc.isTactic (env : Environment) (kind : Name) : Bool

Check whether a name is a tactic syntax kind

opaque Lean.Parser.Tactic.Doc.tacticAlternativeExt : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap Name)

Stores a collection of tactic alternatives, to track which new syntax rules represent new forms of existing tactics.

def Lean.Parser.Tactic.Doc.alternativeOfTactic (env : Environment) (tac : Name) : Option Name

If tac is registered as the alternative form of another tactic, then return the canonical name for it.

def Lean.Parser.Tactic.Doc.aliases {m : Type → Type} [Monad m] [MonadEnv m] (tac : Name) : m NameSet

Find all alternatives for a given canonical tactic name.

opaque Lean.Parser.Tactic.Doc.knownTacticTagExt : PersistentEnvExtension (Name × String × Option String) (Name × String × Option String) (NameMap (String × Option String))

The known tactic tags that allow tactics to be grouped by purpose.

def Lean.Parser.Tactic.Doc.tagInfo {m : Type → Type} [Monad m] [MonadEnv m] (tag : Name) : m (Option (String × Option String))

Get the user-facing name and docstring for a tactic tag.

def Lean.Parser.Tactic.Doc.allTags {m : Type → Type} [Monad m] [MonadEnv m] : m (List Name)

Enumerate the tactic tags that are available

def Lean.Parser.Tactic.Doc.allTagsWithInfo {m : Type → Type} [Monad m] [MonadEnv m] : m (List (Name × String × Option String))

Enumerate the tactic tags that are available, with their user-facing name and docstring

opaque Lean.Parser.Tactic.Doc.tacticTagExt : PersistentEnvExtension (Name × Name) (Name × Name) (NameMap NameSet)

The mapping between tags and tactics. Tags may be applied in any module, not just the defining module for the tactic.

Because this is expected to be augmented regularly, but queried rarely (only when generating documentation indices), it is just stored as flat unsorted arrays of pairs. Before it is used for some other purpose, consider a new representation.

The first projection in each pair is the tactic name, and the second is the tag name.

opaque Lean.Parser.Tactic.Doc.tacticDocExtExt : PersistentEnvExtension (Name × Array String) (Name × String) (NameMap (Array String))

Extensions to tactic documentation.

This provides a structured way to indicate that an extensible tactic has been extended (for instance, new cases tried by trivial).

def Lean.Parser.Tactic.Doc.getTacticExtensions (env : Environment) (tactic : Name) : Array String

Gets the extensions declared for the documentation for the given canonical tactic name

def Lean.Parser.Tactic.Doc.getTacticExtensionString (env : Environment) (tactic : Name) : String

Gets the rendered extensions for the given canonical tactic name

opaque Lean.Parser.Tactic.Doc.tacticNameExt : PersistentEnvExtension (Name × String) (Name × String) (NameMap String)

The mapping between tactics and their custom names.

The first projection in each pair is the tactic name, and the second is the custom name.

def Lean.Parser.Tactic.Doc.customTacticName {m : Type → Type} [Monad m] [MonadEnv m] (tac : Name) : m (Option String)

Finds the custom name assigned to tac, or returns none if there is no such custom name.