Zulip Chat Archive

Stream: general

Topic: univ.pi

Floris van Doorn (Mar 07 2021 at 23:59):

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?

Last updated: Aug 03 2023 at 10:10 UTC