dotParam RFC

Stream: mathlib4

[Kyle Miller]

In case anyone doesn't follow #lean4, the #lean4 > dotParam @ 💬 topic is about an RFC to be able to configure which argument is used for dot notation.

The expected applications are to SetLike/FunLike API (since one can export generic definitions into a namespace specifically for dot notation), and I think it would be useful for the graph theory library.