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