## Stream: general

### Topic: weird hover behavior in vs-code

#### Eric Wieser (Mar 18 2021 at 13:17):

Why does hovering over ⋂ give set.Inter : Π {β ι : Type u_2}, (ι → set β) → set β here? Why did β and ι get forced into the same universe, despite docs#set.Inter putting them in different universes?

import algebra.module.basic

variables {R M : Type*} [semiring R] [add_comm_monoid M] [semimodule R M] (S : set (submodule R M))

#check ⋂ s ∈ S, (s : set M)  -- combined universes?
#check (set.Inter $λ s, set.Inter$ λ (h : s ∈ S), (s : set M))  -- separate universes


Last updated: May 10 2021 at 19:16 UTC