From 358233872b16c7b09a83e07c84f40880d3239171 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Rafa=C3=ABl=20Bocquet?= Date: Fri, 8 Jul 2016 09:30:49 +0200 Subject: [PATCH] Fix conv --- Eval.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Eval.hs b/Eval.hs index 740682c..9203c90 100644 --- a/Eval.hs +++ b/Eval.hs @@ -794,9 +794,6 @@ instance Convertible Val where conv ns u v = let j = fresh (u,v) in case (u,v) of - (Ter (Lam x a u) e,Ter (Lam x' a' u') e') -> - let v@(VVar n _) = mkVarNice ns x (eval e a) - in conv (n:ns) (eval (upd (x,v) e) u) (eval (upd (x',v) e') u') (Ter (Split _ p _ _) e,Ter (Split _ p' _ _) e') -> (p == p') && conv ns e e' (Ter (Sum p _ _) e,Ter (Sum p' _ _) e') -> (p == p') && conv ns e e' (Ter (HSum p _ _) e,Ter (HSum p' _ _) e') -> (p == p') && conv ns e e' @@ -831,6 +828,9 @@ instance Convertible Val where (VUnGlueElem u ts,VUnGlueElem u' ts') -> conv ns (u,ts) (u',ts') (VCompU u es,VCompU u' es') -> conv ns (u,es) (u',es') _ | u == v -> True + (Ter (Lam x a u) e,Ter (Lam x' a' u') e') -> + let v@(VVar n _) = mkVarNice ns x (eval e a) + in conv (n:ns) (eval (upd (x,v) e) u) (eval (upd (x',v) e') u') (Ter (Lam x a u) e,u') -> let v@(VVar n _) = mkVarNice ns x (eval e a) in conv (n:ns) (eval (upd (x,v) e) u) (app u' v) -- 2.34.1