nomeata
parse scoped notation
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).
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.
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.
