Documentation

Lean.Server.Completion

Identifier that is sent from the server to the client as part of the CompletionItem.data? field. Needed to resolve the CompletionItem when the client sends a completionItem/resolve request for that item, again containing the data? field provided by the server.

Instances For

    CompletionItemData that also contains a CompletionIdentifier. See the documentation ofCompletionItemData and CompletionIdentifier.

    Instances For

      Fills the CompletionItem.detail? field of item using the pretty-printed type identified by id.

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

        Cached header declarations for which allowCompletion headerEnv decl is true.

        Returns the declarations in the header for which allowCompletion env decl is true, caching them if not already cached.

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

          Intermediate state while completions are being computed.

          Instances For
            @[reducible, inline]

            Monad used for completion computation that allows modifying a completion State and reading CompletionParams.

            Equations
            Instances For
              def Lean.Server.Completion.matchNamespace (ns : Lake.Name) (nsFragment : Lake.Name) (danglingDot : Bool) :
              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Compares n₁ and n₂ modulo private prefixes. Similar to Name.cmp but ignores all private prefixes in both names. Necessary because the namespaces of private names do not contain private prefixes.

                    NameSet where names are compared according to cmpModPrivate. Helps speed up dot completion because it allows us to look up names without first having to strip the private prefix from deep in the name, letting us reject most names without having to scan the full name first.

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

                        Fills the CompletionItem.detail? field of item using the pretty-printed type identified by id in the context found at hoverPos in infoTree.

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