Tell loogle to exclude something from search result

Stream: general

[Jz Pan]

Is it possible to tell loogle to exclude something from search result? For example, I want to search something mentioning IntermediateField.adjoin and Membership.mem, but not Fintype. It is natural to input the search condition IntermediateField.adjoin, Membership.mem, -Fintype. But it doesn't recognize this pattern. Is there any way to do such search?

[Joachim Breitner]

No, not yet. It’s certainly doable, I am basically trying to assess how often the need comes up, and whether it’s worth it the additional complexity for users learning the query language.

[Joachim Breitner]

I noted the request at https://github.com/nomeata/loogle/issues/6

[Kenny Lau]

I've run into this just now, I want to search for instances of using RingHomClass to construct data, so I wanted to type: RingHomClass, !⊢ (_ : Prop)

[Kenny Lau]

now I was able to do it in a more complicated way:

1. Search for RingHomClass and RingHomClass, ⊢ (_ : Prop)
2. Compare the difference using the following:
3. paste each result in https://regexr.com/ and list occurrences of .+📋
4. paste each result into each side of https://www.diffchecker.com/text-compare/
5. compare

[Joachim Breitner]

In this case, would

RingHomClass, ⊢ (_ : Type _)

serve you well? (Granted, this may probably miss things that are in Sort u for arbitrary u. Not sure.)

[Kenny Lau]

aha, that does work