mathlib
2924a0e4 - Remove name_set and rb_set unioning utility functions

Commit

5 years ago

Remove name_set and rb_set unioning utility functions `merge` already exists as `union`. `merge_many` was removed and inlined.

Author

JLimperg

Committer

JLimperg

Parents