search

Beluga-lang / McLTT

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

Possible extensions for more interesting impl #174

Open Ailrun opened 2 weeks ago

Ailrun commented 2 weeks ago

Please edit the following list if you have anything more. In the order from simpler to harder

Ailrun commented 1 week ago

We decided to add the propositional equality type