{motive : Lean.Server.CodeActionResolveData → Sort u} →
  (t : Lean.Server.CodeActionResolveData) →
    ((params : Lean.Lsp.CodeActionParams) →
        (providerName : Lean.Name) →
          (providerResultIndex : ℕ) →
            motive { params := params, providerName := providerName, providerResultIndex := providerResultIndex }) →
      motive t