Loogle ignores emptyset

Stream: new members

[Snir Broshi]

Searching for ¬∅.Nonempty on Loogle fails to find docs#Set.not_nonempty_empty, but searching for ¬(∅ : Set _).Nonempty or ¬Set.Nonempty ∅ works. The failure is weird; it says:

Found 9019 declarations mentioning Not. Of these, 9010 match your pattern(s). Of these, only the first 200 are shown.

so it completely ignores everything except for the negation.

The bad query asks it to find a type that has .Nonempty and an instance of EmptyCollection, which maybe it can't do, but I expected it to either work or show an error.

Is this a bug?

[Alex Meiburg]

There's no capacity in Loogle for "a type that mentions a constant with name fragment x", so "something that mentions __.Nonempty" isn't handled. Since it can't infer the type of ∅.Nonempty, I think it quits there and doesn't look for deeper terms it could resolve.

Compare with loogling for (1 : ℝ) ≤ (5 + ?a).ugly. Since it doesn't know what ???.ugly is, it can't resolve the terms inside either, so it just ignores the 5 and the +. But if you do (1 : ℝ) ≤ (Real.pi + ?a).ugly, then it can figure out that Real.pi + ?a must also be a real, and so it can deduce that must be Real.ugly, and then it complains that that doesn't exist.

[Alex Meiburg]

I wouldn't consider it a "bug", since it's just kind of how Lean's elaborator has to work. But yeah I guess you could imagine an improvement here

[Snir Broshi]

So is the "ignoring" behavior in Loogle or Lean itself?