HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.55k stars 141 forks source link

Problem with relevance checking with type constructors #496

Closed algebraic-dev closed 2 months ago

algebraic-dev commented 1 year ago
type Bool {
    true
    false
}

Fun (n: U60) : Type
Fun _ = Bool

Main : Type
Main = Fun 2

Does not triggers a relevance error.