Questions tagged [propositions]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
4 votes
1 answer

Can we completely erase propositions in the type checker?

Related question on semantic side: How much of trouble is Lean's failure of normalization, given that logical consistency is not obviously broken? Suppose we have an impredicative universe of ...
  • 4,750