mathlib
4a864ed0 - fix(tactic/core): mk_simp_attribute: remove superfluous disjunct (#8648)

Commit

4 years ago

fix(tactic/core): mk_simp_attribute: remove superfluous disjunct (#8648) `with_ident_list` already returns `[]` if `with` is not present.

Author

digama0

Parents