search

nomeata / loogle

Mathlib search tool
https://loogle.lean-lang.org/
Apache License 2.0
62 stars 7 forks source link

parse scoped notation #19

Open fpvandoorn opened 2 hours ago

fpvandoorn commented 2 hours ago

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 commented 2 hours ago

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 commented 2 hours ago

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.