Skip to content

Commit ce44f02

Browse files
authored
Upgrade Lean to v4.11.0 (#11)
With v4.11.0, `batteries` is no longer needed. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 16fcb23 commit ce44f02

File tree

4 files changed

+2
-18
lines changed

4 files changed

+2
-18
lines changed

RustLeanModels/Basic.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
-- Copyright Kani Contributors
22
-- SPDX-License-Identifier: Apache-2.0 OR MIT
3-
import Batteries.Data.List
43
open String
54
open List
65
open Nat

lake-manifest.json

Lines changed: 1 addition & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,5 @@
11
{"version": "1.1.0",
22
"packagesDir": ".lake/packages",
3-
"packages":
4-
[{"url": "https://github.com/leanprover-community/batteries",
5-
"type": "git",
6-
"subDir": null,
7-
"scope": "",
8-
"rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
9-
"name": "batteries",
10-
"manifestFile": "lake-manifest.json",
11-
"inputRev": "0f3e143",
12-
"inherited": false,
13-
"configFile": "lakefile.lean"}],
3+
"packages": [],
144
"name": "«rust-lean-models»",
155
"lakeDir": ".lake"}

lakefile.toml

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,5 @@ defaultTargets = ["RustLeanModels"]
44
[leanOptions]
55
pp.unicode.fun = true
66

7-
[[require]]
8-
name = "batteries"
9-
git = "https://github.com/leanprover-community/batteries"
10-
rev = "0f3e143"
11-
127
[[lean_lib]]
138
name = "RustLeanModels"

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.10.0
1+
leanprover/lean4:v4.11.0

0 commit comments

Comments
 (0)