∀ (toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams) (toPartialResultParams : Lean.Lsp.PartialResultParams)
  (title : String) (kind? : Option Lean.Lsp.CodeActionKind) (diagnostics? : Option (Array Lean.Lsp.Diagnostic))
  (isPreferred? : Option Bool) (disabled? : Option Lean.Lsp.CodeActionDisabled) (edit? : Option Lean.Lsp.WorkspaceEdit)
  (command? : Option Lean.Lsp.Command) (data? : Option Lean.Json)
  (toWorkDoneProgressParams_1 : Lean.Lsp.WorkDoneProgressParams)
  (toPartialResultParams_1 : Lean.Lsp.PartialResultParams) (title_1 : String) (kind?_1 : Option Lean.Lsp.CodeActionKind)
  (diagnostics?_1 : Option (Array Lean.Lsp.Diagnostic)) (isPreferred?_1 : Option Bool)
  (disabled?_1 : Option Lean.Lsp.CodeActionDisabled) (edit?_1 : Option Lean.Lsp.WorkspaceEdit)
  (command?_1 : Option Lean.Lsp.Command) (data?_1 : Option Lean.Json),
  ({ toWorkDoneProgressParams := toWorkDoneProgressParams, toPartialResultParams := toPartialResultParams,
        title := title, kind? := kind?, diagnostics? := diagnostics?, isPreferred? := isPreferred?,
        disabled? := disabled?, edit? := edit?, command? := command?, data? := data? } =
      { toWorkDoneProgressParams := toWorkDoneProgressParams_1, toPartialResultParams := toPartialResultParams_1,
        title := title_1, kind? := kind?_1, diagnostics? := diagnostics?_1, isPreferred? := isPreferred?_1,
        disabled? := disabled?_1, edit? := edit?_1, command? := command?_1, data? := data?_1 }) =
    (toWorkDoneProgressParams = toWorkDoneProgressParams_1 ∧
      toPartialResultParams = toPartialResultParams_1 ∧
        title = title_1 ∧
          kind? = kind?_1 ∧
            diagnostics? = diagnostics?_1 ∧
              isPreferred? = isPreferred?_1 ∧
                disabled? = disabled?_1 ∧ edit? = edit?_1 ∧ command? = command?_1 ∧ data? = data?_1)