Negative filters - Githubissues

nomeata / loogle

Mathlib search tool

https://loogle.lean-lang.org/

Apache License 2.0

50 stars 6 forks source link

Negative filters #6

Open nomeata opened 7 months ago

nomeata commented 7 months ago

A reasonable feature request is to be able to prefix filters with, say, -, and then exclude all matches.

Technically doable. Would probably call for a refactoring of the implementation that I have in the back of my head anyways.

I am just hesitant to add complexity to the surface, so at the moment, I’m gauging the demand.

Requested here:

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Tell.20loogle.20to.20exclude.20something.20from.20search.20result/near/404747726

ericrbg commented 6 months ago

Just a +1 to say that this would be nice!