search

owo-lang / minitt-rs

Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust
Apache License 2.0
113 stars 3 forks source link

Universe polymorphism #20

Open ice1000 opened 5 years ago

ice1000 commented 5 years ago

The current implementation of universe level does not satisfy:

Luo also adds a rule for function types which is covariant in the codomain but demands equality in the domain.

(from: https://mazzo.li/epilogue/index.html%3Fp=857&cpage=1.html )