{motive : Lean.Server.Ilean → Sort u} →
  ((version : ℕ) →
      (module : Lean.Name) →
        (directImports : Array Lean.Lsp.ImportInfo) →
          (references : Lean.Lsp.ModuleRefs) →
            (decls : Lean.Lsp.Decls) →
              motive
                { version := version, module := module, directImports := directImports, references := references,
                  decls := decls }) →
    (t : Lean.Server.Ilean) → motive t