In draft file, should box accept a parameter in the term definition. It seems to in the syntax rules (box t : ?).
Does subscript T in the draft file mean that the function takes a parameter of type T?
In the code:
typeCheck_aux (Pair t1 t2) = do r1 <- typeCheck_aux t1 r2 <- typeCheck_aux t2
Why are r1 and r2 (Maybe Type) and not Types when typeCheck_aux :: Term -> TCM Type?
typeCheck_aux (Pair t1 t2) = do r1 <- typeCheck_aux t1 r2 <- typeCheck_aux t2
Why are r1 and r2 (Maybe Type) and not Types when typeCheck_aux :: Term -> TCM Type?