From: Anders Mörtberg <anma7372@r120.math.su.se>
Date: Tue, 16 Oct 2018 11:57:55 +0000 (+0200)
Subject: support hcomp in typechecker
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a5c6f94bfc0da84e214641e0b87aa9649ea114ea;p=cubicaltt.git

support hcomp in typechecker
---

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 12135e7..40050c0 100644
--- 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