documenting notation

Stream: general

[Johan Commelin]

#2581 is the start of a PR that should document how to setup notation in Lean. That made me wonder: can we generate an overview of all notation currently introduced in mathlib? Could we add this to our docs pages? @Rob Lewis @Gabriel Ebner @Bryan Gin-ge Chen

[Rob Lewis]

I was going to answer "no, not without changes to core." Then I realized there's a very hackish way we could sort of do it now, reverse engineering the trick Gabriel added to linkify notation in the docs. But I think the hackish output won't be good enough.

[Rob Lewis]

That is, if we want to do it automatically, we need to change core. If someone wants to write things by hand, of course we can.