more report

[bitonic-mengthesis.git] / examples.ka

diff --git a/examples.ka b/examples.ka
index 45e69e4cb1a2dcf1832e1f54b5e5e37d6c4f14fb..072ab79e364772b077c66b03ec913ba53ab7db7c 100644 (file)
--- a/examples.ka
+++ b/examples.ka
@@ -1,3 +1,4 @@
+------------------------------------------------------------
 -- Naturals
 
 data Nat : * => { zero : Nat | suc : Nat -> Nat }
@@ -6,13 +7,18 @@ one : Nat => (suc zero)
 two : Nat => (suc one)
 three : Nat => (suc two)
 
+------------------------------------------------------------
 -- Binary trees
+
 data Tree : [A : *] -> * =>
   { leaf : Tree A | node : Tree A -> A -> Tree A -> Tree A }
 
+------------------------------------------------------------
 -- Empty types
+
 data Empty : * => { }
 
+------------------------------------------------------------
 -- Ordered lists
 
 record Unit : * => tt { }
@@ -37,11 +43,12 @@ le' [l1 : Lift] : Lift -> * => (
     (\l2    => Lift-Elim l2 (\_ => *) Empty (\_  => Empty)    Unit)
 )
 
-data OList : [low : Lift] [upp : Lift] -> * =>
+data OList : [low upp : Lift] -> * =>
   { nil  : le' low upp -> OList low upp
   | cons : [n : Nat] -> OList (lift n) upp -> le' low (lift n) -> OList low upp
   }
 
+------------------------------------------------------------
 -- Dependent products
 
 record Prod : [A : *] [B : A -> *] -> * =>