From 0bfe1a8c1a2e2eb6da0dad270d7b2bbdd5b97c3d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 15 Oct 2024 12:18:51 +1100 Subject: [PATCH] chore: better default value for Array.swapAt! (#5705) --- src/Init/Data/Array/Basic.lean | 2 +- src/Init/Data/Array/Lemmas.lean | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 69418da8d6..fc0812eee9 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -216,7 +216,7 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α := if h : i < a.size then swapAt a ⟨i, h⟩ v else - have : Inhabited α := ⟨v⟩ + have : Inhabited (α × Array α) := ⟨(v, a)⟩ panic! ("index " ++ toString i ++ " out of bounds") def shrink (a : Array α) (n : Nat) : Array α := diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 478eb877b9..61407ddb40 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -582,6 +582,13 @@ theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]? theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) : a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h] +@[simp] theorem size_swapAt! (a : Array α) (i : Nat) (v : α) : + (a.swapAt! i v).2.size = a.size := by + simp only [swapAt!] + split + · simp + · rfl + @[simp] theorem toList_pop (a : Array α) : a.pop.toList = a.toList.dropLast := by simp [pop] @[deprecated toList_pop (since := "2024-09-09")]