Allow searching for just lemmas or just definitions (I guess: Prop/Sort)

[ericrbg]

It'd be nice to only be shown lemmas when I'm looking for lemmas, as opposed to other stuff that I don't particularly want; I assume it'd be the same for defs!

[nomeata]

Any concrete syntax in mind?

[ericrbg]

Maybe just "lemma" or "def" as special keywords? That should be fine to special-case I guess

[nomeata]

That a reasonable suggestion. If they are “filters” of their own you’d have to comma-searate them, e.g.

theorem, 1 + 1 =2

which probably takes getting used to. Or the syntax could be more liberal and not require a comma after theorem or def.

(Note that lemma is a Mathlib’ism, not a lean keyword. I’ll have to think about whether loogle should be generous or generic here.)

[nomeata]

BTW, the current syntax allows this already, although less convenient: You can write

|- (?a : Prop)

to get theorems and

|- (?a : Type _)

to get everything else.

For example https://loogle.lean-lang.org/?q=Real.sin%2C+%7C-+%28%3Fa+%3A+Prop%29 vs. https://loogle.lean-lang.org/?q=Real.sin%2C+%7C-+%28%3Fa+%3A+Type+_%29.

[ericrbg]

I think having to comma-separate them doesn't seem unreasonable!