Finding implementations of classes / operators in IDE

Stream: new members

[Weiyi Wang]

For regular theorems and definitions, whenever I am curious, I can ctrl+click on the name to look at the implementation detail and verify my understanding. This however doesn't seem to work well for class implementations and operators, as ctrl+click only leads to the class definition, or the notation definition. The "Instances" section in the doc provides a great help (with some additional clicking), but it becomes difficult for some instances.

For example, recently I wanted to verify how \le and \subset are implemented for Multisets (and there is a key difference between the two that I want to be 100% sure I understand correctly). However, the implementation for \le is so big: it is an entire hierarchy of classes (LE, Preorder, PartialOrder...) and the doc only list the implementation on the one according to how the code was written, which in this case can be found in PartialOrder but not in LE.

Sometimes this is made even more difficult if the class is not implemented for the specific type I am working at, but has a blanket implementation applicable to all types satisfying certain other classes. It might not have a guessable name to search for.

How do you work around with this kind of problem?

[Aaron Liu]

I do #synth and set_option pp.explicit true so I can look at the output without clicking through

[Weiyi Wang]

That's a good way. Thanks!

[Kyle Miller]

For mathematical content, there ought to be characterization lemmas somewhere in the library, since you're generally not supposed to expand definitions, but rewrite.

For example, here I searched for 'Multiset.le_iff' in the mathlib docs and found docs#Multiset.le_iff_count

Similarly, I searched for 'Multiset.subset_iff' and found the exact match docs#Multiset.subset_iff

These make the difference between the two very clear. There's also docs#Multiset.subset_of_le nearby to show a logical relationship between them.