From: Anders Mörtberg <mortberg@chalmers.se>
Date: Tue, 14 Apr 2015 20:20:17 +0000 (+0200)
Subject: Undef is neutral (but there is an issue with inferType for undef)
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=ca772fa7c1df9c50d09bf7be356bc54756e0694e;p=cubicaltt.git

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

diff --git a/CTT.hs b/CTT.hs
index b4321a4..c4940da 100644
--- 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