ofFn

@[simp]

theorem Array.toList_ofFn {n : Nat} {α : Type u_1} (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f