mem_pair

Stream: mathlib4

[Dan Velleman]

Is there a reason why mathlib has List.mem_pair and ZFSet.mem_pair, but not Set.mem_pair?

[Kyle Miller]

Here's recent discussion about this: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/More.20API.20for.20pair.20sets.3F/near/418521695 (I'm didn't read all of it, so I'm not sure what sort of conclusion was reached.)

[Eric Rodriguez]

I think it'd be really good for definitions that have fancy non-obvious syntax like this to have much better hovers. (I'm thinking Finsupp.single & update too, which have a really pretty notation, but unless you know what they're formed of, sometimes it's hard to prove things about it)