From: Anders Mörtberg <mortberg@chalmers.se>
Date: Sun, 3 May 2015 16:18:08 +0000 (+0200)
Subject: Add missing spaces
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=27eb9aedc47d7e0afa24c264d0d1de320ce9e86b;p=cubicaltt.git

Add missing spaces
---

diff --git a/examples/mystery.ctt b/examples/mystery.ctt
index e7ea372..d3b76f7 100644
--- a/examples/mystery.ctt
+++ b/examples/mystery.ctt
@@ -138,7 +138,7 @@ c2t2c : (c1 : S1) (c2 : S1) -> IdP (<_> (_ : S1) * S1) (t2c (c2t' c1 c2)) (c1 ,
      loop @ y -> (\ (c : S1) -> c2t2c_loop' c @ y)
 
 S1S1equalsTorus : Id U (and S1 S1) Torus = isoId (and S1 S1) Torus c2t t2c t2c2t rem
-where
+ where
  rem (c:and S1 S1) : Id (and S1 S1) (t2c (c2t c)) c = c2t2c c.1 c.2
 
 
diff --git a/examples/torus.ctt b/examples/torus.ctt
index 8989667..0e98f20 100644
--- a/examples/torus.ctt
+++ b/examples/torus.ctt
@@ -173,5 +173,5 @@ diag_of_image_of_ff : IdP (<_> (_ : S1) * S1) (base,base) (base,base)
 --                             [ (!0 = 0) -> <!1> pathOneT {Torus} @ !1 ])
 
 S1S1equalsTorus : Id U (and S1 S1) Torus = isoId (and S1 S1) Torus c2t t2c t2c2t rem
-where
+ where
  rem (c:and S1 S1) : Id (and S1 S1) (t2c (c2t c)) c = c2t2c c.1 c.2