Merge pull request #70 from leanprover-community/bump_to_v4.16.0

chore: bump toolchain to v4.16.0
leanprover-community · Feb 4, 2025 · eed8e6f · eed8e6f
2 parents 4d7e572 + 51879e1
commit eed8e6f
Show file tree

Hide file tree

Showing 6 changed files with 11 additions and 11 deletions.
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0-rc2
+leanprover/lean4:v4.16.0
diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "15f16b1ec50f425147926be1aede7b4baa725380",
+   "rev": "a6276f4c6097675b1cf5ebd49b1146b735f38c02",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc2",
+   "inputRev": "v4.16.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
+   "rev": "1a6613663c3eb08c401ce0fd1a408412f2c2321e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c104265c34eb8181af14e8dbc14c2f034292cb02",
+   "rev": "01006c9e86bf9e397c026fef4190478dd1fd897e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml
@@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.16.0-rc2"
+rev = "v4.16.0"
 
 [[lean_lib]]
 name = "ReplMathlibTests"

diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0-rc2
+leanprover/lean4:v4.16.0
diff --git a/test/Mathlib/test/H20231020.in b/test/Mathlib/test/H20231020.in
@@ -2,7 +2,7 @@
 
 {"cmd": "theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num", "env": 0}
 
-{"cmd": "theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})", "env": 0}
+{"cmd": "theorem mathd_numbertheory_403 : ∑ k ∈ (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})", "env": 0}
 
-{"cmd": "theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k in Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]", "env": 0}
+{"cmd": "theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k ∈ Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]", "env": 0}
 
diff --git a/test/Mathlib/test/H20231020.lean b/test/Mathlib/test/H20231020.lean
@@ -17,6 +17,6 @@ open Topology
 
 theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num
 
-theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})
+theorem mathd_numbertheory_403 : ∑ k ∈ (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})
 
-theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k in Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]
+theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k ∈ Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.16.0-rc2
		leanprover/lean4:v4.16.0