mathlib3
14f324be - chore(data/set/basic): remove set.decidable_mem (#8240)

Commit
4 years ago
chore(data/set/basic): remove set.decidable_mem (#8240) The only purpose of this instance was to enable the spelling `[decidable_pred s]` when what is actually needed is `decidable_pred (∈ s)`, which is a bad idea. This is a follow-up to #8211. Only two proofs needed this instance, and both were using completely the wrong lemmas anyway.
Author
Parents
Loading