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

Check whether a name is a tactic syntax kind

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

Enumerate the tactic tags that are available

Equations

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

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

Equations

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

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

Equations

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

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

Gets the rendered extensions for the given canonical tactic name

Equations

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

def Lean.Parser.Tactic.Doc.getTacticExtensionString.indentLine (str : String) : String

Equations

• Lean.Parser.Tactic.Doc.getTacticExtensionString.indentLine str = (if (str.all fun (x : Char) => x.isWhitespace) = true then str else " " ++ str) ++ "\n"

def Lean.Parser.Tactic.Doc.getTacticExtensionString.bullet (str : String) : String

Equations

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

def Lean.Parser.Tactic.Doc.tacticDocsOnTactics : ParserAttributeHook

Validates that a tactic alternative is actually a tactic and that syntax tagged as tactics are tactics.

Equations

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