From ca772fa7c1df9c50d09bf7be356bc54756e0694e Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 14 Apr 2015 22:20:17 +0200 Subject: [PATCH] Undef is neutral (but there is an issue with inferType for undef) --- CTT.hs | 1 + 1 file changed, 1 insertion(+) 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 -- 2.34.1