{motive : Lean.Server.FileWorker.MemorizedInteractiveDiagnostics → Sort u} →
  (t : Lean.Server.FileWorker.MemorizedInteractiveDiagnostics) →
    ((diags : Array Lean.Widget.InteractiveDiagnostic) → motive { diags := diags }) → motive t