Documentation

Lean.Parser.Tactic.Doc

Check whether a name is a tactic syntax kind

Equations
    Instances For

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

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

      Equations
        Instances For

          Find all alternatives for a given canonical tactic name.

          Equations
            Instances For

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

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

              Equations
                Instances For

                  Enumerate the tactic tags that are available

                  Equations
                    Instances For

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

                      Equations
                        Instances For

                          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.

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

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

                          Equations
                            Instances For

                              Gets the rendered extensions for the given canonical tactic name

                              Equations
                                Instances For

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

                                  Equations
                                    Instances For