catvayor
Results
2
comments of
catvayor
Shouldn't `?[n]. maybe ([n]t)` be illegal ? For me, `maybe ([n]t)` doesn't witness `n` as it doesn't guaranty to have an array of size `n`.
As I understood witnessing, sum type should witness the intersection of every constructor witnesses. This said, there's still an error in the typing of the ite in the example, shouldn't...