mathlib
fbc95927 - chore(data/list): move some sections to separate files (#2341)

Commit
5 years ago
chore(data/list): move some sections to separate files (#2341) * move list.func namespace to its own file * move erase_dup to its own file * move rotate to its own file * move tfae to its own file * move bag_inter and intervals * move range out * move nodup * move chain and pairwise * move zip * move forall2 * move of_fn * add copyright headers * remove unnecessary sections, move defns to func.set and tfae * fixes * oops, forgot to add file Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading