An improved search engine for Lean:
I haven’t used it yet but it looks promising.
I personally don’t like the search on mathlib4_docs and find it very glitchy, slow, and cumbersome.
Normally, I just use grep in VSCode instead, which is better but still very cumbersome and requires a lot of regex jujitsu.
Hopefully this search is better and more useful.
Looking forward to trying it out.