search

Beluga-lang / McLTT

A bottom-up approach to a verified implementation of MLTT
https://beluga-lang.github.io/McLTT/
MIT License
14 stars 2 forks source link

Do we have consistency and canonical forms? #233

Closed HuStmpHrrr closed 2 days ago

HuStmpHrrr commented 3 days ago

I can't find the theorems for them.

Ailrun commented 3 days ago

For pi type, https://github.com/Beluga-lang/McLTT/blob/main/theories/Core/Semantic/Consequences.v#L48 But for others, I don't think we have one.

HuStmpHrrr commented 2 days ago

I suppose we don't have consistency? Is there one?

Ailrun commented 2 days ago

Now we have. (https://beluga-lang.github.io/McLTT//Mcltt.Core.Semantic.Consequences.html#consistency)