univ.pi

Stream: general

[Floris van Doorn]

Does someone know why univ.pi is interpreted as the nonexistent set.univ.pi instead of projection notation for pi univ?

import data.set.basic
open set
example {α} {β : α → Type*} (t : Π i, set (β i)) : univ.pi t = ∅ := sorry

Even (univ).pi and ( univ ).pi fail. However, (univ : _).pi or (@univ _).pi are interpreted correctly.
Is this a bug?