Fix add_comm

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 4eb75e44035a05cf0c5bc0f857bd39a98e5aac0a..da38d53ec9e2d2804cce0997d8e0163cf1de1079 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -247,7 +247,7 @@ checkCompSystem :: System Val -> Typing ()
 checkCompSystem vus = do\r
   ns <- asks names\r
   unless (isCompSystem ns vus)\r
-    (throwError $ "Incompatible system " ++ show vus)\r
+    (throwError $ "Incompatible system " ++ showSystem vus)\r
 \r
 -- Check the values at corresponding faces with a function, assumes\r
 -- systems have the same faces\r

diff --git a/examples/add.ctt b/examples/add.ctt
index e55cb9f97a78f0d0924c303231a9b2210363274c..1fa272c3003bdf0d3a68d9d46809adf8a53afb0d 100644 (file)
--- a/examples/add.ctt
+++ b/examples/add.ctt
@@ -16,37 +16,38 @@ add_suc (a:nat) : (n : nat) -> Id nat (add (suc a) n) (suc (add a n)) = split
 
 add_comm (a : nat) : (n : nat) -> Id nat (add a n) (add n a) = split
   zero  -> <i> add_zero a @ -i
-  suc m -> <i> comp nat (suc (add_comm a m @ i)) [ (i = 1) -> <j> add_suc m a @ -j]
+  suc m -> <i> comp nat (suc (add_comm a m @ i)) [ (i = 0) -> <j> suc (add a m),
+                                                   (i = 1) -> <j> add_suc m a @ -j]
 
 assocAdd (a b:nat) : (c:nat) -> Id nat (add a (add b c)) (add (add a b) c) = split
  zero -> <i>add a b
  suc c1 -> <i>suc (assocAdd a b c1@i)
 
 
-test (A:U) (a b c d e : A) (p:Id A a b) (q:Id A b c) (r:Id A c d) (s:Id A d e) : Id A a e =
- <i>comp A (p@i) [ (i=1) -> <i>comp A (q@i) [ (i=1) -> <i>comp A (r@i) [ (i=1) -> s]]]
+-- test (A:U) (a b c d e : A) (p:Id A a b) (q:Id A b c) (r:Id A c d) (s:Id A d e) : Id A a e =
+--  <i>comp A (p@i) [ (i=1) -> <i>comp A (q@i) [ (i=1) -> <i>comp A (r@i) [ (i=1) -> s]]]
 
-data tree = leaf | bin (t0 t1:tree)
+-- data tree = leaf | bin (t0 t1:tree)
 
-swap : tree -> tree = split
- leaf -> leaf
- bin t0 t1 -> bin (swap t1) (swap t0)
+-- swap : tree -> tree = split
+--  leaf -> leaf
+--  bin t0 t1 -> bin (swap t1) (swap t0)
 
-lem : (t:tree) -> Id tree (swap (swap t)) t = split
- leaf -> <i>leaf
- bin t0 t1 -> <i>bin (lem t0@i) (lem t1@i)
+-- lem : (t:tree) -> Id tree (swap (swap t)) t = split
+--  leaf -> <i>leaf
+--  bin t0 t1 -> <i>bin (lem t0@i) (lem t1@i)
 
-pred : nat -> nat = split
- zero -> zero
- suc n -> n
+-- pred : nat -> nat = split
+--  zero -> zero
+--  suc n -> n
 
-simplAdd (b c :nat) : (a : nat) -> Id nat (add b a) (add c a) -> Id nat b c = split
- zero -> \ (h:Id nat b c) -> h
- suc a1 -> \ (h : Id nat (suc (add b a1)) (suc (add c a1))) -> simplAdd b c a1 (<i>pred (h@i))
+-- simplAdd (b c :nat) : (a : nat) -> Id nat (add b a) (add c a) -> Id nat b c = split
+--  zero -> \ (h:Id nat b c) -> h
+--  suc a1 -> \ (h : Id nat (suc (add b a1)) (suc (add c a1))) -> simplAdd b c a1 (<i>pred (h@i))
 
-corSimplAdd (b c a :nat) (h: Id nat (add a b) (add a c)) : Id nat b c =  simplAdd b c a rem
- where rem : Id nat (add b a) (add c a) = 
-          <i>comp nat ((add_comm b a)@i) [(i=1) -> <i>comp nat (h@i) [(i=1) -> add_comm a c]]
+-- corSimplAdd (b c a :nat) (h: Id nat (add a b) (add a c)) : Id nat b c =  simplAdd b c a rem
+--  where rem : Id nat (add b a) (add c a) = 
+--           <i>comp nat ((add_comm b a)@i) [(i=1) -> <i>comp nat (h@i) [(i=1) -> add_comm a c]]
  
 
-leq (b c:nat) : U = (a : nat) * Id nat (add a b) c
\ No newline at end of file
+-- leq (b c:nat) : U = (a : nat) * Id nat (add a b) c
\ No newline at end of file

diff --git a/examples/nat.ctt b/examples/nat.ctt
index f36e78dbf0e90dc660534cb55097f8de4d98bf1d..dec9d9289168726c1be4dc293aa42589cdaf925d 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -1,6 +1,6 @@
 module nat where
 
-import hedberg
+import prelude
 
 data nat = zero | suc (n : nat)
 
@@ -53,4 +53,4 @@ natDec : (n m:nat) -> dec (Id nat n m) = split
    (\ (m:nat) -> decEqCong (Id nat n m) (Id nat (suc n) (suc m)) (\ (p:Id nat n m) -> <i> suc (p @ i))
                  (sucInj n m) (natDec n m))
 
-natSet : set nat = hedberg nat natDec
+-- natSet : set nat = hedberg nat natDec