mathlib
299af47c - chore(data/fin/basic): move tuple stuff to a new file (#10295)

Commit
4 years ago
chore(data/fin/basic): move tuple stuff to a new file (#10295) There are almost 600 lines of tuple stuff, which is definitely sufficient to justify a standalone file. The author information has been guessed from the git history. Floris is responsible for `cons` and `tail` which came first in #1294, Chris added find, and Yury and Sébastien were involved all over the place. This is simply a cut-and-paste job, with the exception of the new module docstring which has been merged with the docstring for the tuple subheading.
Author
Parents
Loading