Merge pull request #56 from leanprover-community/batteries

chore: update Std->Batteries

ProofWidgets/Demos/SelectInsertConv.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robin Böhne, Wojciech Nawrocki, Patrick Massot
 -/
 import Lean.Meta.ExprLens
-import Std.Lean.Position
+import Batteries.Lean.Position
 import ProofWidgets.Data.Html
 import ProofWidgets.Component.OfRpcMethod
 import ProofWidgets.Component.MakeEditLink

lake-manifest.json

@@ -1,11 +1,11 @@
 {"version": 7,
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "3025cb124492b423070f20cf0a70636f757d117f",
-   "name": "std",
+   "rev": "56d2e4ee226603eb6b90b05f6b944bde42672cd5",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,

lakefile.lean

@@ -10,7 +10,7 @@ lean_lib ProofWidgets
 lean_lib ProofWidgets.Demos where
   globs := #[.submodules `ProofWidgets.Demos]
 
-require std from git "https://github.com/leanprover/std4" @ "main"
+require batteries from git "https://github.com/leanprover-community/batteries" @ "main"
 
 def npmCmd : String :=
   if Platform.isWindows then "npm.cmd" else "npm"