Documentation

Lean.Parser.Attr

@[inline]
Equations
    Instances For
      @[inline]
      Equations
        Instances For
          Equations
            Instances For
              Equations
                Instances For
                  Equations
                    Instances For
                      Equations
                        Instances For
                          Equations
                            Instances For
                              Equations
                                Instances For
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For
                                          Equations
                                            Instances For
                                              Equations
                                                Instances For

                                                  Declare this tactic to be an alias or alternative form of an existing tactic.

                                                  This has the following effects:

                                                  • The alias relationship is saved
                                                  • The docstring is taken from the original tactic, if present
                                                  Equations
                                                    Instances For

                                                      Add one or more tags to a tactic.

                                                      Tags should be applied to the canonical names for tactics.

                                                      Equations
                                                        Instances For