Type dependent notation

Stream: new members

[Olonbayar Temuulen]

Can anyone give me a good reference to understand what it means to "The meaning of this notation is type dependent"?

[Eric Wieser]

Can you give some context on where you saw that sentence?

[llllvvuu]

I usually see that pop up when I hover over + or • or something. Basically means e.g. + needs to be defined for the specific types A and B if you are trying to add a: A and b: B.

You'll need to learn about: https://lean-lang.org/theorem_proving_in_lean/type_classes.html

[llllvvuu]

(I think the infoview should technically know which e.g. HSMul is being used, but I don't remember how to access that)