Undef is neutral (but there is an issue with inferType for undef)

diff --git a/CTT.hs b/CTT.hs
index b4321a4ff6340c1663ae8e8f25c309fdbb19d9a3..c4940da5b1ddad66ab4c69486f65c32e56f121f7 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -165,6 +165,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