Fix undefined

diff --git a/CTT.hs b/CTT.hs
index 176651c6acb34ea0a6b127e0d5ff50f858f2bd6e..ee1f020590eec484a53a44f6ac98cd3c6313d5ff 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -167,6 +167,7 @@ data Val = VU
 
 isNeutral :: Val -> Bool
 isNeutral v = case v of
+  Ter Undef{} _     -> True
   VVar _ _          -> True
   VFst v            -> isNeutral v
   VSnd v            -> isNeutral v

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 39e920be1eb777f3cb727f1ec42d6f9044749580..407f7af4e3d3b492348c49fafae833b05f96f91f 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -143,6 +143,7 @@ evalTyping t = eval <$> asks env <*> pure t
 -- Check that t has type a\r
 check :: Val -> Ter -> Typing ()\r
 check a t = case (a,t) of\r
+  (_,Undef{}) -> return ()\r
   (_,Con c es) -> do\r
     (bs,nu) <- getLblType c a\r
     checks (bs,nu) es\r
@@ -359,7 +360,7 @@ infer :: Ter -> Typing Val
 infer e = case e of\r
   U         -> return VU  -- U : U\r
   Var n     -> lookType n <$> asks env\r
-  Undef _ t -> evalTyping t\r
+--  Undef _ t -> evalTyping t\r
   App t u -> do\r
     c <- infer t\r
     case c of\r