Zulip Chat Archive

Stream: general

Topic: fillter types?


view this post on Zulip Kenny Lau (Feb 17 2019 at 08:28):

So we don't need to write the universes every time and Lean automatically generates them for us (the names would be u_1, etc)... what if Lean did the same to types?

view this post on Zulip Chris Hughes (Feb 17 2019 at 08:33):

Generally Lean just gives every Type a different universe variable. You don't want it giving every variable a different Type. It seems like a much harder problem.


Last updated: May 15 2021 at 00:39 UTC