Convertability for HSum

diff --git a/Eval.hs b/Eval.hs
index 4f28dbfdc637890d134e8749aad82b5f9d24a9bd..c1479eb8bf23ba446c271b8ea9d6538b52c5ec93 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -594,6 +594,7 @@ instance Convertible Val where
         in conv (n:ns) (app u' v) (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'
       (Ter (Undef p _) e,Ter (Undef p' _) e') -> p == p' && conv ns e e'
       (Ter (Hole p) e,Ter (Hole p') e') -> p == p' && conv ns e e'
       -- (Ter Hole{} e,_) -> True