chore: bump lean

Mathport/Binary/ParseTLean.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Daniel Selsam, Gabriel Ebner
 -/
 import Lean
-import Std.Data.List.Basic
+import Batteries.Data.List.Basic
 import Mathport.Util.Parse
 import Mathport.Binary.Basic
 import Mathport.Binary.EnvModification

Mathport/Syntax/Translate/Expr.lean

@@ -94,21 +94,21 @@ def trExtBinders (args : Array (Spanned Binder)) : M Syntax := do
   | ⟨_, Binder.collection bi vars n rhs⟩ =>
     if let some g := predefinedBinderPreds.find? n then
       onVars vars fun v =>
-        return #[← `(Std.ExtendedBinder.extBinder|
+        return #[← `(Batteries.ExtendedBinder.extBinder|
           $(trBinderIdent v):binderIdent $(g (← trExpr rhs)):binderPred)]
     else
       expandBinderCollection trBasicBinder bi vars n rhs
   | ⟨_, Binder.notation _⟩ => warn! "unsupported: (notation) binder" | pure #[]
-  if let #[bi] := out then `(Std.ExtendedBinder.extBinders| $bi:extBinder)
-  else `(Std.ExtendedBinder.extBinders| $[($out:extBinder)]*)
+  if let #[bi] := out then `(Batteries.ExtendedBinder.extBinders| $bi:extBinder)
+  else `(Batteries.ExtendedBinder.extBinders| $[($out:extBinder)]*)
 where
   onVars {α} (vars) (f : BinderName → M (Array α)) : M (Array α) := do
     if vars.size > 1 then
       warn! "warning: expanding binder group ({spaced repr vars})"
     vars.concatMapM (fun ⟨_, v⟩ => f v)
   trBasicBinder (vars ty) :=
     onVars vars fun v =>
-      return #[← `(Std.ExtendedBinder.extBinder|
+      return #[← `(Batteries.ExtendedBinder.extBinder|
         $(trBinderIdent v):binderIdent $[: $(← ty.mapM fun ty => trExpr ty)]?)]
 
 partial def trFunBinder : Binder → M (Array Syntax.FunBinder)

Mathport/Syntax/Translate/Notation.lean

@@ -6,7 +6,7 @@ Authors: Mario Carneiro
 import Mathport.Util.Json
 import Mathport.Util.Misc
 import Mathlib.Mathport.Syntax
-import Std.Util.ExtendedBinder
+import Batteries.Util.ExtendedBinder
 import Mathlib.Data.Set.Lattice
 
 open Lean

Oneshot/lean4-in/lake-manifest.json

@@ -8,10 +8,10 @@
    "dir": "./../../.lake/packages/Qq",
    "configFile": "lakefile.lean"},
   {"type": "path",
-   "name": "std",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inherited": false,
-   "dir": "./../../.lake/packages/std",
+   "dir": "./../../.lake/packages/batteries",
    "configFile": "lakefile.lean"},
   {"type": "path",
    "name": "aesop",

Oneshot/lean4-in/lakefile.lean

@@ -6,7 +6,7 @@ package extra
 @[default_target] lean_lib Extra
 
 require Qq from ".." / ".." / ".lake" / "packages" / "Qq"
-require std from ".." / ".." / ".lake" / "packages" / "std"
+require batteries from ".." / ".." / ".lake" / "packages" / "batteries"
 require aesop from ".." / ".." / ".lake" / "packages" / "aesop"
 require proofwidgets from ".." / ".." / ".lake" / "packages" / "proofwidgets"
 require importGraph from ".." / ".." / ".lake" / "packages" / "importGraph"

config-project.json

@@ -10,7 +10,7 @@
         "leanPath": [
             "./.lake/packages/mathlib/.lake/build/lib",
             "./.lake/packages/Qq/.lake/build/lib",
-            "./.lake/packages/std/.lake/build/lib",
+            "./.lake/packages/batteries/.lake/build/lib",
             "./.lake/packages/aesop/.lake/build/lib",
             "./.lake/packages/proofwidgets/.lake/build/lib",
             "./.lake/packages/importGraph/.lake/build/lib",

config.json

@@ -11,7 +11,7 @@
         "leanPath": [
             "./.lake/packages/mathlib/.lake/build/lib",
             "./.lake/packages/Qq/.lake/build/lib",
-            "./.lake/packages/std/.lake/build/lib",
+            "./.lake/packages/batteries/.lake/build/lib",
             "./.lake/packages/aesop/.lake/build/lib",
             "./.lake/packages/proofwidgets/.lake/build/lib",
             "./.lake/packages/importGraph/.lake/build/lib",

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": "789020bc2f7fbc330e33818075a94381da04de4e",
-   "name": "std",
+   "rev": "56d2e4ee226603eb6b90b05f6b944bde42672cd5",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -22,19 +22,19 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
+   "rev": "2225b0e4a3528da20499e2304b521e0c4c2a4563",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fe1eff53bd0838c657aa6126fe4dd75ad9939d9a",
+   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.35",
+   "inputRev": "v0.0.36",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "7cec59317b9e4f2abbacb986c904614a113e8507",
+   "rev": "c46d22bbe4f8363c0829ce0eb48a95012cdc0d79",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "4199e29c92ebe1352ac437120f82f1b9eb005857",
+   "rev": "9edd2350d9396700cf5a446372b94f082479154c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",