Closed lukaszcz closed 1 year ago
This has to do with how we type things for case-on
. The term index 1
in the left term will be typed in the context so1, so1, (coprod so1 so1)
so that it will take on type so1
causing a mistyping. The correct way to write this term will be:
(app (lamb (list (coprod so1 so1)) (case-on (index 0) (lamb (list so1) (index 2)) (lamb (list so1) (left so1 (unit))))) (list (right so1 (unit))))
i.e. simply changing the depth of the index.
What am I doing wrong here?