no goals
α✝ : Type u_1
f : α✝ → α✝
acc : Array α✝
n : Nat
⊢ modifyNthTR.go f [] n acc = acc.data ++ modifyNth f n []
cases n <;> simp [modifyNthTR.go, modifyNth]
no goals
α✝ : Type u_1
f : α✝ → α✝
acc : Array α✝
a : α✝
l : List α✝
⊢ modifyNthTR.go f (a :: l) 0 acc = acc.data ++ modifyNth f 0 (a :: l)
simp [modifyNthTR.go, modifyNth]
no goals
α✝ : Type u_1
f : α✝ → α✝
acc : Array α✝
a : α✝
l : List α✝
n : Nat
⊢ modifyNthTR.go f (a :: l) (n + 1) acc = acc.data ++ modifyNth f (n + 1) (a :: l)
simp [modifyNthTR.go, modifyNth, modifyNthTR_go_eq l]