From ffa2d9635d358274433cece34fa326a49794ab62 Mon Sep 17 00:00:00 2001
From: Francesco Mazzoli <f@mazzo.li>
Date: Fri, 14 Jun 2013 13:23:59 +0100
Subject: foo

---
 examples.ka | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'examples.ka')

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
 
-- 
cgit v1.2.3