From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 20 Oct 2016 21:19:01 +0000 (-0400)
Subject: comments
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9a706dceece08db06c42c2bb8f5bbe68a9ec87fb;p=cubicaltt.git

comments
---

diff --git a/examples/circle.ctt b/examples/circle.ctt
index 5748481..6254432 100644
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -1,14 +1,12 @@
+-- The circle as a HIT.
 module circle where
 
 import bool
 import int
 
-              ----------------------------------
-              -- Example: The circle as a HIT --
-              ----------------------------------
-
 data S1 = base
-        | loop <i> [(i=0) -> base, (i=1) -> base]
+        | loop <i> [ (i=0) -> base
+                   , (i=1) -> base]
 
 loopS1 : U = Path S1 base base
 
diff --git a/examples/csystem.ctt b/examples/csystem.ctt
index 80ba0a1..2158a97 100644
--- a/examples/csystem.ctt
+++ b/examples/csystem.ctt
@@ -1,5 +1,7 @@
+-- Definition of C-systems and universe categories. Construction of a
+-- C-system from a universe category.
 module csystem where
-import prelude
+
 import sigma
 import equiv
 import nat