diff options
| -rw-r--r-- | LeanAStar/HashSet.lean | 2 | ||||
| -rw-r--r-- | lake-manifest.json | 4 | ||||
| -rw-r--r-- | lakefile.toml | 4 | ||||
| -rw-r--r-- | 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 |