Documentation

Init.Data.Array.BasicAux

theorem Array.of_push_eq_push {α : Type u_1} {a : α} {b : α} {as : Array α} {bs : Array α} (h : Array.push as a = Array.push bs b) :
as = bs a = b
@[simp]
theorem List.toArray_eq_toArray_eq {α : Type u_1} (as : List α) (bs : List α) :
(List.toArray as = List.toArray bs) = (as = bs)