Documentation

Lean.Server.CodeActions.Attr

Initial setup for code action attributes #

@[reducible, inline]

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
      @[reducible, inline]

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

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

          • declName : Lake.Name

            The declaration to tag

          • cmdKinds : Array Lake.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