`zip_with_take_{l,r,both}{,'}` (was: Add lemma `zip_with_take_both`) (!339) · Merge requests · Iris / stdpp

Merged Glen Mével requested to merge gmevel/stdpp:glen/zip_with_take_both into master 3 years ago

Status	Pipeline	Stages
Passed 00:10:11 3 years ago	update changelog w.r.t. `zip_with_take_*` changes #58183 339 d49329c7	Stage: build	Download artifacts No artifacts found
Passed 00:04:39 3 years ago	specialize `zip_with_take_{l,r,both}` and generalize them into `zip_with_take_{l,r,both}'` #58003 339 4573b15f	Stage: build	Download artifacts No artifacts found
Passed 00:04:32 3 years ago	Apply 1 suggestion(s) to 1 file(s) #57857 339 282d96fd	Stage: build	Download artifacts No artifacts found
Passed 00:09:57 3 years ago	Add lemma `zip_with_take_both` #57850 339 74bed0ee	Stage: build	Download artifacts No artifacts found

`zip_with_take_{l,r,both}{,'}` (was: Add lemma `zip_with_take_both`)