From: Anders Mörtberg <mortberg@chalmers.se>
Date: Mon, 20 Apr 2015 08:12:57 +0000 (+0200)
Subject: Fix all the old examples of HITs
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d5d7b5f88af921768e85e79d2df3beda987ddcc5;p=cubicaltt.git

Fix all the old examples of HITs
---

diff --git a/examples/circle.ctt b/examples/circle.ctt
index 758e412..44da52b 100644
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -4,7 +4,7 @@ import bool
 import int
 
 data S1 = base
-        | loop @ base ~ base
+        | loop <i> [(i=0) -> base, (i=1) -> base]
 
 loopS1 : U = Id S1 base base
 
diff --git a/examples/higherhit.ctt b/examples/higherhit.ctt
index e6993bd..4b6b085 100644
--- a/examples/higherhit.ctt
+++ b/examples/higherhit.ctt
@@ -7,7 +7,7 @@ import prelude
 -- old stuff looks now like this
 
 data S1 = base
-        | loop <i> @ [(i=0) -> base, (i=1) -> base]
+        | loop <i> [(i=0) -> base, (i=1) -> base]
 
 
 foo : S1 = base
@@ -18,25 +18,25 @@ loop' : Id S1 base base = <i> (loop {S1}) @ i
 -- new
 
 data S2 = base
-        | loop2 <i j> @ [ (i=0) -> base
-                        , (i=1) -> base
-                        , (j=0) -> base
-                        , (j=1) -> base]
+        | loop2 <i j> [ (i=0) -> base
+                      , (i=1) -> base
+                      , (j=0) -> base
+                      , (j=1) -> base]
 
 loop2' : Id (Id S2 base base) (refl S2 base) (refl S2 base) =
   <i j> loop2 {S2} @ i @ j
 
 data Torus = ptT
-           | pathOneT <i> @ [ (i=0) -> ptT, (i=1) -> ptT ]
-           | pathTwoT <i> @ [ (i=0) -> ptT, (i=1) -> ptT ]
-           | squareT <i j> @ [ (i=0) -> pathOneT {Torus} @ j
-                             , (i=1) -> pathOneT {Torus} @ j
-                             , (j=0) -> pathTwoT {Torus} @ i
-                             , (j=1) -> pathTwoT {Torus} @ i ]
+           | pathOneT <i> [ (i=0) -> ptT, (i=1) -> ptT ]
+           | pathTwoT <i> [ (i=0) -> ptT, (i=1) -> ptT ]
+           | squareT <i j> [ (i=0) -> pathOneT {Torus} @ j
+                           , (i=1) -> pathOneT {Torus} @ j
+                           , (j=0) -> pathTwoT {Torus} @ i
+                           , (j=1) -> pathTwoT {Torus} @ i ]
 
 data setTrunc (A : U)
   = inc (a : A)
-  | setTr (a b : setTrunc A) (p q : Id (setTrunc A) a b) <i j> @
+  | setTr (a b : setTrunc A) (p q : Id (setTrunc A) a b) <i j>
        [ (i=0) -> p @ j
        , (i=1) -> q @ j
        , (j=0) -> a
diff --git a/examples/integer.ctt b/examples/integer.ctt
index e3d4d8b..57c5db2 100644
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -4,7 +4,7 @@ import int
 
 data int = pos (n : nat)
          | neg (n : nat)
-         | zeroP @ pos zero ~ neg zero
+         | zeroP <i> [(i=0) -> pos zero, (i=1) -> neg zero]
 
 zeroP' : Id int (pos zero) (neg zero) = <i> zeroP {int} @ i
 
diff --git a/examples/interval.ctt b/examples/interval.ctt
index d5a2c43..ca455da 100644
--- a/examples/interval.ctt
+++ b/examples/interval.ctt
@@ -2,7 +2,7 @@ module interval where
 
 import prelude
 
-data I = zero | one | seg @ zero ~ one
+data I = zero | one | seg <i> [(i = 0) -> zero, (i = 1) -> one]
 
 -- Proof of funext from the interval
 fext (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) :
diff --git a/examples/susp.ctt b/examples/susp.ctt
index ef53a7a..1224b14 100644
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -4,7 +4,7 @@ import circle
 
 data susp (A : U) = north
                   | south
-                  | merid (a:A) @ north ~ south
+                  | merid (a:A) <i> [(i=0) -> north, (i=1) -> south]
 
 -- n-spheres
 sphere : nat -> U = split