Commit 2021-05-11 21:05 6470fee8

View on Github →

feat(Data/Array/Basic): add toArrayLit_eq from doomed PR lean#390

Estimated changes

added theorem Array.data_toArray
added theorem Array.ext'
added theorem Array.toArrayLit_eq
added theorem List.toArrayAux_data
added theorem List.toArray_data
added theorem List.concat_eq_append
added theorem List.drop_eq_nil_of_le
added theorem List.get_cons_drop