Upgrade Lean to v4.11.0

zhassan-aws · zhassan-aws · commit fd5cff834931 · 2024-09-03T12:17:52.000-07:00
diff --git a/RustLeanModels/Basic.lean b/RustLeanModels/Basic.lean
@@ -1,6 +1,5 @@
 -- Copyright Kani Contributors
 -- SPDX-License-Identifier: Apache-2.0 OR MIT
-import Batteries.Data.List
 open String
 open List
 open Nat
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -1,15 +1,5 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "0f3e143",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+ "packages": [],
  "name": "«rust-lean-models»",
  "lakeDir": ".lake"}
diff --git a/lakefile.toml b/lakefile.toml
@@ -4,10 +4,5 @@ defaultTargets = ["RustLeanModels"]
 [leanOptions]
 pp.unicode.fun = true
 
-[[require]]
-name = "batteries"
-git = "https://github.com/leanprover-community/batteries"
-rev = "0f3e143"
-
 [[lean_lib]]
 name = "RustLeanModels"
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.11.0
