From: Simon Huber <hubsim@gmail.com>
Date: Wed, 10 Jun 2015 09:21:36 +0000 (+0200)
Subject: Convertability for HSum
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=854ce1724f3ec3d8a8d14ade04ebfa6c638f9bc9;p=cubicaltt.git

Convertability for HSum
---

diff --git a/Eval.hs b/Eval.hs
index 4f28dbf..c1479eb 100644
--- 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