X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=examples.ka;fp=examples.ka;h=cedf81a91ce79026172e159e4788727e77376949;hb=ffa2d9635d358274433cece34fa326a49794ab62;hp=072ab79e364772b077c66b03ec913ba53ab7db7c;hpb=fb4e0b4b2daac3838f6161836298cd4d1bf54766;p=bitonic-mengthesis.git

diff --git a/examples.ka b/examples.ka
index 072ab79..cedf81a 100644
--- 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