Documentation

Batteries.CodeAction.Attr

Initial setup for code action attributes #

@[reducible, inline]

A tactic code action extension.

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

    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
      • One or more equations did not get rendered due to their size.
      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