...

[bitonic-mengthesis.git] / examples.ka

diff --git a/examples.ka b/examples.ka
index cedf81a91ce79026172e159e4788727e77376949..e0370cc5360573b86e1b69a59b9da7b4a2499cc5 100644 (file)
--- a/examples.ka
+++ b/examples.ka
@@ -1,58 +1,58 @@
 ------------------------------------------------------------
 -- Naturals
 
-data Nat : * => { zero : Nat | suc : Nat -> Nat }
+data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }
 
-one : Nat => (suc zero)
-two : Nat => (suc one)
-three : Nat => (suc two)
+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 }
+data Tree : [A : ⋆] → ⋆ ⇒
+  { leaf : Tree A | node : Tree A → A → Tree A → Tree A }
 
 ------------------------------------------------------------
 -- Empty types
 
-data Empty : * => { }
+data Empty : ⋆ ⇒ { }
 
 ------------------------------------------------------------
 -- Ordered lists
 
-record Unit : * => tt { }
+record Unit : ⋆ ⇒ tt { }
 
-le [n : Nat] : Nat -> * => (
+le [n : Nat] : Nat → ⋆ ⇒ (
   Nat-Elim
     n
-    (\_ => Nat -> *)
-    (\_ => Unit)
-    (\n f m => Nat-Elim m (\_ => *) Empty (\m' _ => f m'))
+    (λ _ ⇒ Nat → ⋆)
+    (λ _ ⇒ Unit)
+    (λ n f m ⇒ Nat-Elim m (λ _ ⇒ ⋆) Empty (λ m' _ ⇒ f m'))
 )
 
-data Lift : * =>
-  { bot : Lift | lift : Nat -> Lift | top : Lift }
+data Lift : ⋆ ⇒
+  { bot : Lift | lift : Nat → Lift | top : Lift }
 
-le' [l1 : Lift] : Lift -> * => (
+le' [l1 : Lift] : Lift → ⋆ ⇒ (
   Lift-Elim
     l1
-    (\_ => Lift -> *)
-    (\_     => Unit)
-    (\n1 l2 => Lift-Elim l2 (\_ => *) Empty (\n2 => le n1 n2) Unit)
-    (\l2    => Lift-Elim l2 (\_ => *) Empty (\_  => Empty)    Unit)
+    (λ _ ⇒ Lift → ⋆)
+    (λ _     ⇒ Unit)
+    (λ n1 l2 ⇒ Lift-Elim l2 (λ _ ⇒ ⋆) Empty (λ n2 ⇒ le n1 n2) Unit)
+    (λ l2    ⇒ Lift-Elim l2 (λ _ ⇒ ⋆) Empty (λ _  ⇒ Empty)    Unit)
 )
 
-data OList : [low upp : Lift] -> * =>
-  { onil  : le' low upp -> OList low upp
-  | ocons : [n : Nat] -> OList (lift n) upp -> le' low (lift n) -> OList low upp
+data OList : [low upp : Lift] → ⋆ ⇒
+  { 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 }
+data List : [A : ⋆] → ⋆ ⇒
+  { nil : List A | cons : A → List A → List A }
 
 ------------------------------------------------------------
 -- Dependent products
 
-record Prod : [A : *] [B : A -> *] -> * =>
+record Prod : [A : ⋆] [B : A → ⋆] → ⋆ ⇒
   prod {fst : A, snd : B fst}