Commit 2022-12-07 01:05 655994e2
View on Github →refactor(data/set/n_ary): extract from data/set/basic (#17836)
This is essentially just a copy paste, with one or two whitespace fixes.
This split is consistent with how finset/n_ary
is its own file, and does a nice job of making data/set/basic
a bit shorter.
The comment fixes referring to this new file are thanks to #17825.