Loogle feature request: hide deprecated aliasses

Stream: lean4

[Michael Rothgang]

Suppose I'm looking for misnamed lemmas. As one example, I might want to look for lemmas which mention an "IsOpen" hypothesis, but have "of_open" as part of their name. If I @loogle IsOpen, "of_open", the results include all deprecated aliasses. How difficult would it be to allow me to hide those?

[Joachim Breitner]

I'm hesitant to make it configurable, but a point could be made to simply ignore all ignored identifiers. Feel free to open an issue against Loogle to that end

[Michael Rothgang]

I just saw your answer now. Sure, that's also reasonable; I've commented on the existing issue https://github.com/nomeata/loogle/issues/34.