Compare commits

...

1 Commits

Author SHA1 Message Date
Kim Morrison
c60922fb66 chore: restore @[simp] on Array.swapAt!_def 2024-09-25 11:15:43 +10:00

View File

@@ -481,7 +481,7 @@ theorem get?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)[k]?
@[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
a.swapAt i v = (a[i.1], a.set i v) := rfl
-- @[simp] -- FIXME: gives a weird linter error
@[simp]
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]