Topic: fillter types?
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?
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