Fix all the old examples of HITs

diff --git a/examples/circle.ctt b/examples/circle.ctt
index 758e41225c08d013f18dfc2eca832e88fce89d6f..44da52b151cb6a5d9cf3083e45d6844d4b3aa683 100644 (file)
--- 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 e6993bd6cdc11541575e22e94ec2485b20dfd385..4b6b0856506f8276d5e4df3cf2b5ce52119abe1d 100644 (file)
--- 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 e3d4d8bcf6c03ed68360edb6664c6aeae36364fa..57c5db258910b5008e978a52131ead29412fa95a 100644 (file)
--- 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 d5a2c43718c630c1ecce1dbb367f614b8552a32a..ca455da5520a4e25d98ac09747946cd960004772 100644 (file)
--- 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 ef53a7afe1388a14caf9a24971cadf7144e03ef0..1224b1499b8fd0b058a6beee4f2fcf8915ee210c 100644 (file)
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -4,7 +4,7 @@ import circle
 \r
 data susp (A : U) = north\r
                   | south\r
-                  | merid (a:A) @ north ~ south\r
+                  | merid (a:A) <i> [(i=0) -> north, (i=1) -> south]\r
 \r
 -- n-spheres\r
 sphere : nat -> U = split\r