foo

[bitonic-mengthesis.git] / examples.ka

diff --git a/examples.ka b/examples.ka
index 072ab79e364772b077c66b03ec913ba53ab7db7c..cedf81a91ce79026172e159e4788727e77376949 100644 (file)
--- a/examples.ka
+++ b/examples.ka
@@ -44,10 +44,13 @@ le' [l1 : Lift] : 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
+  { onil  : le' low upp -> OList low upp
+  | ocons : [n : Nat] -> OList (lift n) upp -> le' low (lift n) -> OList low upp
   }
 
+data List : [A : *] -> * =>
+  { nil : List A | cons : A -> List A -> List A }
+
 ------------------------------------------------------------
 -- Dependent products