Documentation

Std.CodeAction.Attr

Initial setup for code action attributes #

@[inline, reducible]

A hole code action extension.

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

    Read a hole code action from a declaration of the right type.

    Equations
    Instances For
      @[inline, reducible]

      A tactic code action extension.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[inline, reducible]

        A tactic code action extension.

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

          Read a tactic code action from a declaration of the right type.

          Equations
          Instances For

            Read a tacticSeq code action from a declaration of the right type.

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

              An entry in the tactic code actions extension, containing the attribute arguments.

              • declName : Lean.Name

                The declaration to tag

              • tacticKinds : Array Lean.Name

                The tactic kinds that this extension supports. If empty it is called on all tactic kinds.

              Instances For

                The state of the tactic code actions extension.

                Instances For

                  Insert a tactic code action entry into the TacticCodeActions structure.

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

                    This attribute marks a code action, which is used to suggest new tactics or replace existing ones.

                    • @[tactic_code_action]: This is a code action which applies to the spaces between tactics, to suggest a new tactic to change the goal state.

                    • @[tactic_code_action kind]: This is a code action which applies to applications of the tactic kind (a tactic syntax kind), which can replace the tactic or insert things before or after it.

                    • @[tactic_code_action kind₁ kind₂]: shorthand for @[tactic_code_action kind₁, tactic_code_action kind₂].

                    • @[tactic_code_action *]: This is a tactic code action that applies to all tactics. Use sparingly.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[inline, reducible]

                      A command code action extension.

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

                        Read a command code action from a declaration of the right type.

                        Equations
                        Instances For

                          An entry in the command code actions extension, containing the attribute arguments.

                          • declName : Lean.Name

                            The declaration to tag

                          • cmdKinds : Array Lean.Name

                            The command kinds that this extension supports. If empty it is called on all command kinds.

                          Instances For

                            The state of the command code actions extension.

                            Instances For

                              Insert a command code action entry into the CommandCodeActions structure.

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

                                This attribute marks a code action, which is used to suggest new tactics or replace existing ones.

                                • @[command_code_action kind]: This is a code action which applies to applications of the command kind (a command syntax kind), which can replace the command or insert things before or after it.

                                • @[command_code_action kind₁ kind₂]: shorthand for @[command_code_action kind₁, command_code_action kind₂].

                                • @[command_code_action]: This is a command code action that applies to all commands. Use sparingly.

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