Ah is that what Lean does with its type universes? | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		IshKebab 3 months ago \| parent \| context \| favorite \| on: Typechecking is undecideable when 'type' is a type... Ah is that what Lean does with its type universes?

cjfd 3 months ago [–]

Yes, it is.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact