Zulip Chat Archive

Stream: general

Topic: weird hover behavior in vs-code

view this post on Zulip 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