parse scoped notation

[fpvandoorn]

It would be nice if the parser is aware of scoped notation.
Examples:
_ ↓∩ _
𝓝 _
ℝ≥0∞

One complication: overloaded scoped notation (but I'm happy if it doesn't work in that case).

[nomeata]

Hmm, but aren't these scoped for a reason?

The feature I could see here is that you can specify which namespaces were opened, and then it'll just work. Tedious to use from the web interface, but #loogle might actually easily do that under the hood.

[fpvandoorn]

Honestly I'm not sure how good the reason is that these are scoped, beyond "maybe someone else will come along one day that wants to use a different meaning for these notations". In Mathlib these do not conflict with any other notation, and are opened very liberally and practically anywhere they are used.

The namespace-aware #loogle sounds very useful.