chore: some NameSet API has been upstreamed

ImportGraph/RequiredModules.lean

@@ -7,28 +7,7 @@ import Lean.CoreM
 import Lean.Data.NameMap
 import Lean.Environment
 import Lean.Util.FoldConsts
-
-namespace Lean.NameSet
-
-instance : Singleton Name NameSet where
-  singleton := fun n => (∅ : NameSet).insert n
-
-instance : Union NameSet where
-  union := fun s t => s.fold (fun t n => t.insert n) t
-
-instance : Inter NameSet where
-  inter := fun s t => s.fold (fun r n => if t.contains n then r.insert n else r) {}
-
-instance : SDiff NameSet where
-  sdiff := fun s t => t.fold (fun s n => s.erase n) s
-
-def ofList (l : List Name) : NameSet :=
-  l.foldl (fun s n => s.insert n) {}
-
-def ofArray (a : Array Name) : NameSet :=
-  a.foldl (fun s n => s.insert n) {}
-
-end Lean.NameSet
+import Batteries.Data.NameSet
 
 namespace Lean
 

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8ce422eb59adf557fac184f8b1678c75fa03075c",
+   "rev": "66225aab4f6bd1687053b03916105f7cab140507",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",

lakefile.toml

@@ -14,7 +14,7 @@ rev = "main"
 [[require]]
 name = "batteries"
 scope = "leanprover-community"
-rev = "v4.16.0-rc1"
+rev = "main"
 
 [[lean_lib]]
 name = "ImportGraph"