How to loogle for exists `∃`

Stream: lean4

[Markus Schmaus]

How can I loogle for patterns involving ∃?

Let's say I'm looking for a lemma with the conclusion of docs#Quot.exists_rep, I would try out |- ∃ (?a : ?α), Quot.mk ?r ?a = ?q, but this results in an error message, I guess this is because of the comma ,. So is there a way to do this?

[Markus Schmaus]

(deleted)

[Damiano Testa]

Maybe...

@loogle Exists, Quot

[loogle]

:search: Quot.exists_rep, Multiset.exists_multiset_eq_map_quot_mk, and 2 more

[Markus Schmaus]

There are ways to find docs#Quot.exists_rep. The question is: how do I specify patterns involving ∃?

[Markus Schmaus]

Here is another:
@loogle Quot.mk ?r ?a = ?q

[loogle]

:search: Quot.exists_rep, Quot.sound, and 43 more

[Eric Wieser]

You should be searching for |- ∃ (a : ?α), Quot.mk ?r ?a = ?q

[Eric Wieser]

The first a isn't a wildcard, it's a binder