Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-12 23:17 bc77a23e

View on Github →

feat(data/list/*): add left- and right-biased versions of map₂ and zip (#4512) When given lists of different lengths, map₂ and zip truncate the output to the length of the shorter input list. This commit adds variations on map₂ and zip whose output is always as long as the left/right input.

Estimated changes

Modified src/data/list/basic.lean

added theorem list.map₂_flip

added theorem list.map₂_left'_nil_right

added theorem list.map₂_left_eq_map₂

added theorem list.map₂_left_eq_map₂_left'

added theorem list.map₂_left_nil_right

added theorem list.map₂_right'_cons_cons

added theorem list.map₂_right'_nil_cons

added theorem list.map₂_right'_nil_left

added theorem list.map₂_right'_nil_right

added theorem list.map₂_right_cons_cons

added theorem list.map₂_right_eq_map₂

added theorem list.map₂_right_eq_map₂_right'

added theorem list.map₂_right_nil_cons

added theorem list.map₂_right_nil_left

added theorem list.map₂_right_nil_right

added theorem list.zip_left'_cons_cons

added theorem list.zip_left'_cons_nil

added theorem list.zip_left'_nil_left

added theorem list.zip_left'_nil_right

added theorem list.zip_left_cons_cons

added theorem list.zip_left_cons_nil

added theorem list.zip_left_eq_zip_left'

added theorem list.zip_left_nil_left

added theorem list.zip_left_nil_right

added theorem list.zip_right'_cons_cons

added theorem list.zip_right'_nil_cons

added theorem list.zip_right'_nil_left

added theorem list.zip_right'_nil_right

added theorem list.zip_right_cons_cons

added theorem list.zip_right_eq_zip_right'

added theorem list.zip_right_nil_cons

added theorem list.zip_right_nil_left

added theorem list.zip_right_nil_right

Modified src/data/list/defs.lean

added def list.map₂_left'

added def list.map₂_left

added def list.map₂_right'

added def list.map₂_right

added def list.zip_left'

added def list.zip_left

added def list.zip_right'

added def list.zip_right