From 27eb9aedc47d7e0afa24c264d0d1de320ce9e86b Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Sun, 3 May 2015 18:18:08 +0200 Subject: [PATCH] Add missing spaces --- examples/mystery.ctt | 2 +- examples/torus.ctt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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) -> 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 -- 2.34.1