From 2402a88a863e41f5bceefcdc13323ef609809a8a Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Thu, 9 Oct 2025 22:53:27 +0200 Subject: Lean 4.18 --- LeanAStar/HashSet.lean | 2 +- lake-manifest.json | 4 ++-- lakefile.toml | 4 ++-- lean-toolchain | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/LeanAStar/HashSet.lean b/LeanAStar/HashSet.lean index 33ef316..c73216e 100644 --- a/LeanAStar/HashSet.lean +++ b/LeanAStar/HashSet.lean @@ -100,7 +100,7 @@ theorem size_le_finite_set_size {α : Type u} [Finite α] [BEq α] [LawfulBEq α exact Std.HashSet.size_le_finite_worker_size α set ⟨l,h.substr $ Nat.lt_succ_self l⟩ (λa hx ↦ by have h₁ := a.isLt - simp_arith[h] at h₁ + simp +arith[h] at h₁ have h₂ : a > l := Fin.lt_iff_val_lt_val.mp hx exact absurd h₁ (Nat.not_le.mpr h₂) ) diff --git a/lake-manifest.json b/lake-manifest.json index a0ff74c..723a9b7 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,11 +1,11 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/soulsource/BinaryHeap", + [{"url": "http://git.grois.info/BinaryHeap", "type": "git", "subDir": null, "scope": "", - "rev": "7896480adb78fc9f9b7a86a5eddd0fc5e3f9e4d5", + "rev": "60832223e03e50cbffca8bc90b1dec40b48f1f14", "name": "BinaryHeap", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lakefile.toml b/lakefile.toml index f4fe843..957dbdd 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -14,5 +14,5 @@ name = "LeanAStarTest" [[require]] name = "BinaryHeap" -git = "https://github.com/soulsource/BinaryHeap" -revision = "7896480adb78fc9f9b7a86a5eddd0fc5e3f9e4d5" \ No newline at end of file +git = "http://git.grois.info/BinaryHeap" +revision = "60832223e03e50cbffca8bc90b1dec40b48f1f14" \ No newline at end of file diff --git a/lean-toolchain b/lean-toolchain index db29c97..9f78e65 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.17.0 +leanprover/lean4:4.18.0 -- cgit v1.2.3