Add missing spaces

diff --git a/examples/mystery.ctt b/examples/mystery.ctt
index e7ea3727c381466bf5f1b4686d1d353fb3aa4d76..d3b76f7e65bf9ac14545d40988dfafd000d9c33a 100644 (file)
--- 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 8989667c6d72ece032a64256ec53ca73dc9451ff..0e98f203aba30bc622b9a0c284451b9eb3234cbc 100644 (file)
--- 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