Documentation

Lean.Server.CodeActions.Attr

Initial setup for code action attributes #

@[reducible, inline]

A hole code action extension.

Equations
    Instances For

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

      Equations
        Instances For
          @[reducible, inline]

          A command code action extension.

          Equations
            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 : Name

                    The declaration to tag

                  • cmdKinds : Array 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
                        Instances For
                          Equations
                            Instances For