diff options
| -rw-r--r-- | LeanAStar/Finite.lean | 2 | ||||
| -rw-r--r-- | lake-manifest.json | 2 | ||||
| -rw-r--r-- | lakefile.toml | 2 | ||||
| -rw-r--r-- | lean-toolchain | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/LeanAStar/Finite.lean b/LeanAStar/Finite.lean index 302e3b1..cbd8ee3 100644 --- a/LeanAStar/Finite.lean +++ b/LeanAStar/Finite.lean @@ -187,7 +187,7 @@ protected theorem Finite.set_worker_size (α : Type u) [Finite α] [BEq α] [Has subst n have h₂ := h₂ ⟨m+1,h₁⟩ (Fin.le_refl _) have hx := Std.HashSet.mem_iff_contains.mp hx - exact absurd hx (Bool.eq_false_iff.mp h₂) + exact absurd hx h₂ termination_by _ n => n.val theorem Finite.set_size_eq_cardinality (α : Type u) [Finite α] [BEq α] [Hashable α] [LawfulBEq α] : (Finite.set α).size = Finite.cardinality α := by diff --git a/lake-manifest.json b/lake-manifest.json index be02118..0e55485 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "93c883d5332469d90a4f1c42d45c66e2b6a89eb8", + "rev": "79f6af06385585087f08a7d77eb43d8674c16948", "name": "BinaryHeap", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lakefile.toml b/lakefile.toml index c252c82..6dafdc4 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -12,4 +12,4 @@ name = "LeanAStarTest" [[require]] name = "BinaryHeap" git = "http://git.grois.info/BinaryHeap" -revision = "93c883d5332469d90a4f1c42d45c66e2b6a89eb8"
\ No newline at end of file +revision = "79f6af06385585087f08a7d77eb43d8674c16948"
\ No newline at end of file diff --git a/lean-toolchain b/lean-toolchain index a0922e9..6c721df 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.19.0 +leanprover/lean4:4.20.1 |