support hcomp in typechecker

mortberg · Oct 16, 2018 · a5c6f94 · a5c6f94
1 parent d48d58d
commit a5c6f94
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/TypeChecker.hs b/TypeChecker.hs
@@ -483,6 +483,12 @@ infer e = case e of
     check va0 t0
     checkPLamSystem t0 va ps
     return va1
+  HComp a u0 us -> do
+    check VU a
+    va <- evalTyping a
+    check va u0
+    checkPLamSystem u0 (constPath va) us
+    return va
   Fill a t0 ps -> do
     (va0, va1) <- checkPLam (constPath VU) a
     va <- evalTyping a