Commit 2021-05-11 23:07 21ff8c55

View on Github →

feat(Data/List): versions of list functions with lean 3 style defeq

Estimated changes

added def List.append'
added theorem List.append'_eq_append
added theorem List.concat_eq_append'
modified theorem List.concat_eq_append
modified theorem List.drop_eq_nil_of_le
added def List.length'
added theorem List.length'_eq_length