no goals
α : Type u_1
a : Array α
⊢ size (pop a) = size a - 1
match a with
| ⟨[]⟩ => rfl
| ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
no goals
α : Type u_1
a : Array α
⊢ size (pop { data := List.nil }) = size { data := List.nil } - 1
rfl
no goals
α : Type u_1
a✝ : Array α
a : α
as : List α
⊢ size (pop { data := a :: as }) = size { data := a :: as } - 1
simp [pop, Nat.succ_sub_succ_eq_sub, size]