Poll: new feature on LeanSearch

Stream: general

[Tony Beta Lambda]

Here are several possible new features we are planning on LeanSearch, and we want to know your thoughts on them!

1. Search by formal name. For example, search "semi" and get semigroups, semirings, seminorms, etc.
2. Provide support for libraries other than mathlib.
3. Add clickable links to referenced constants (like doc-gen).

[Kevin Buzzard]

What would FLT need to do in order to be supported? Would we need changes at our end?

[Bolton Bailey]

Clickable links and the ability to add new libraries would be my preferences, in that order. Search by formal name is fairly well covered by other tools, in my personal opinion.