mathlib
cdad1104 - feat(tactic/equiv_rw): enhancing 'equiv_rw' (#11730)

Commit
3 years ago
feat(tactic/equiv_rw): enhancing 'equiv_rw' (#11730) Expands the `equiv_rw` API by: * Making it accept a list of equivalences instead of a single one, if intended * Allowing multiple targets (closes #2891) Extra: some optimizations.
Author
Parents
Loading