{motive : Lean.Lsp.ServerCapabilities → Sort u} →
  (t : Lean.Lsp.ServerCapabilities) →
    ((textDocumentSync? : Option Lean.Lsp.TextDocumentSyncOptions) →
        (completionProvider? : Option Lean.Lsp.CompletionOptions) →
          (hoverProvider documentHighlightProvider documentSymbolProvider definitionProvider declarationProvider
              typeDefinitionProvider referencesProvider callHierarchyProvider : Bool) →
            (renameProvider? : Option Lean.Lsp.RenameOptions) →
              (workspaceSymbolProvider foldingRangeProvider : Bool) →
                (semanticTokensProvider? : Option Lean.Lsp.SemanticTokensOptions) →
                  (codeActionProvider? : Option Lean.Lsp.CodeActionOptions) →
                    (inlayHintProvider? : Option Lean.Lsp.InlayHintOptions) →
                      (signatureHelpProvider? : Option Lean.Lsp.SignatureHelpOptions) →
                        (colorProvider? : Option Lean.Lsp.DocumentColorOptions) →
                          (experimental? : Option Lean.Lsp.LeanServerCapabilities) →
                            motive
                              { textDocumentSync? := textDocumentSync?, completionProvider? := completionProvider?,
                                hoverProvider := hoverProvider, documentHighlightProvider := documentHighlightProvider,
                                documentSymbolProvider := documentSymbolProvider,
                                definitionProvider := definitionProvider, declarationProvider := declarationProvider,
                                typeDefinitionProvider := typeDefinitionProvider,
                                referencesProvider := referencesProvider,
                                callHierarchyProvider := callHierarchyProvider, renameProvider? := renameProvider?,
                                workspaceSymbolProvider := workspaceSymbolProvider,
                                foldingRangeProvider := foldingRangeProvider,
                                semanticTokensProvider? := semanticTokensProvider?,
                                codeActionProvider? := codeActionProvider?, inlayHintProvider? := inlayHintProvider?,
                                signatureHelpProvider? := signatureHelpProvider?, colorProvider? := colorProvider?,
                                experimental? := experimental? }) →
      motive t