From: Anders Mörtberg <mortberg@chalmers.se>
Date: Wed, 3 Jun 2015 18:48:42 +0000 (+0200)
Subject: Fix add_comm
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=b33373043246fb044be6d645a97b908924eeb7ee;p=cubicaltt.git

Fix add_comm
---

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 4eb75e4..da38d53 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -247,7 +247,7 @@ checkCompSystem :: System Val -> Typing ()
 checkCompSystem vus = do
   ns <- asks names
   unless (isCompSystem ns vus)
-    (throwError $ "Incompatible system " ++ show vus)
+    (throwError $ "Incompatible system " ++ showSystem vus)
 
 -- Check the values at corresponding faces with a function, assumes
 -- systems have the same faces
diff --git a/examples/add.ctt b/examples/add.ctt
index e55cb9f..1fa272c 100644
--- 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 f36e78d..dec9d92 100644
--- 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