From: Anders Mörtberg Date: Wed, 20 Sep 2017 11:11:20 +0000 (+0200) Subject: cleaning X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=69cb2ef9dacdcebe3e1bdc224f03d9dfa9ae6bcc;p=cubicaltt.git cleaning --- diff --git a/examples/integer.ctt b/examples/integer.ctt index 8892377..33f69e5 100644 --- a/examples/integer.ctt +++ b/examples/integer.ctt @@ -10,7 +10,8 @@ import int data int = pos (n : nat) | neg (n : nat) - | zeroP [(i=0) -> pos zero, (i=1) -> neg zero] + | zeroP [ (i = 0) -> pos zero + , (i = 1) -> neg zero ] -- Nice version of the zero constructor: zeroZ : Path int (pos zero) (neg zero) = zeroP {int} @ i @@ -44,15 +45,15 @@ fromZ : Z -> int = split inr n -> pos n toZK : (a : Z) -> Path Z (toZ (fromZ a)) a = split - inl n -> refl Z (inl n) - inr n -> refl Z (inr n) + inl n -> <_> inl n + inr n -> <_> inr n fromZK : (a : int) -> Path int (fromZ (toZ a)) a = split - pos n -> refl int (pos n) + pos n -> <_> pos n neg n -> rem n where rem : (n : nat) -> Path int (fromZ (toZ (neg n))) (neg n) = split zero -> zeroZ - suc m -> refl int (neg (suc m)) + suc m -> <_> neg (suc m) zeroP @ i -> zeroZ @ i /\ j isoIntZ : Path U Z int = isoPath Z int fromZ toZ fromZK toZK @@ -62,11 +63,11 @@ intSet : set int = subst U set Z int isoIntZ ZSet -- a concrete instance T : U = Path int (pos zero) (pos zero) -p0 : T = refl int (pos zero) +p0 : T = <_> pos zero p1 : T = compPath int (pos zero) (neg zero) (pos zero) zeroZ (zeroZ@-i) -test0 : Path (Path Z (inr zero) (inr zero)) (refl Z (inr zero)) (refl Z (inr zero)) = - ZSet (inr zero) (inr zero) (refl Z (inr zero)) (refl Z (inr zero)) +test0 : Path (Path Z (inr zero) (inr zero)) (<_> inr zero) (<_> inr zero) = + ZSet (inr zero) (inr zero) (<_> inr zero) (<_> inr zero) -- Tests for normal forms: test1 : Path T p0 p1 = intSet (pos zero) (pos zero) p0 p1 diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 0c8a77d..4c3a480 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -150,11 +150,11 @@ Square (A : U) (a0 a1 b0 b1 : A) = PathP ( (PathP ( A) (u @ i) (v @ i))) r0 r1 constSquare (A : U) (a : A) (p : Path A a a) : Square A a a a a p p p p = - comp (A) a - [(i = 0) -> p @ (j \/ - k), - (i = 1) -> p @ (j /\ k), - (j = 0) -> p @ (i \/ - k), - (j = 1) -> p @ (i /\ k)] + comp (<_> A) a + [ (i = 0) -> p @ j \/ - k + , (i = 1) -> p @ j /\ k + , (j = 0) -> p @ i \/ - k + , (j = 1) -> p @ i /\ k ] prop (A : U) : U = (a b : A) -> Path A a b set (A : U) : U = (a b : A) -> prop (Path A a b)