Commit 2025-01-21 03:27 6e428275

View on Github →

chore(Data/List/Basic): split off Map2 lemmas (#20832) This PR splits off a number of lemmas related maps that zip pairs of lists from Data.List.Basic to a new file, including:

  • map₂Left'
  • map₂Right'
  • zipWith
  • zipLeft'
  • zipRight' Doing so reduces the size of this long file by ~250 lines. Also note that the new file doesn't need to import Basic, so this should parallelize the compilation too.

Estimated changes

deleted theorem List.map₂Left_nil_right
deleted theorem List.map₂Right_nil_cons
deleted theorem List.map₂Right_nil_left
deleted theorem List.nil_zipWith
deleted theorem List.zipLeft'_cons_cons
deleted theorem List.zipLeft'_cons_nil
deleted theorem List.zipLeft'_nil_left
deleted theorem List.zipLeft'_nil_right
deleted theorem List.zipLeft_cons_cons
deleted theorem List.zipLeft_cons_nil
deleted theorem List.zipLeft_eq_zipLeft'
deleted theorem List.zipLeft_nil_left
deleted theorem List.zipLeft_nil_right
deleted theorem List.zipRight'_cons_cons
deleted theorem List.zipRight'_nil_cons
deleted theorem List.zipRight'_nil_left
deleted theorem List.zipRight'_nil_right
deleted theorem List.zipRight_cons_cons
deleted theorem List.zipRight_nil_cons
deleted theorem List.zipRight_nil_left
deleted theorem List.zipRight_nil_right
deleted theorem List.zipWith_flip
deleted theorem List.zipWith_nil
added theorem List.nil_zipWith
added theorem List.zipLeft'_cons_nil
added theorem List.zipLeft'_nil_left
added theorem List.zipLeft_cons_cons
added theorem List.zipLeft_cons_nil
added theorem List.zipLeft_nil_left
added theorem List.zipLeft_nil_right
added theorem List.zipRight_nil_cons
added theorem List.zipRight_nil_left
added theorem List.zipWith_flip
added theorem List.zipWith_nil