source
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.

Instances For

source
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.

source
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.

Instances For

source
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.

Instances For

source
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.

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

source
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`).

source
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.

Instances For

source
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.

Instances For