examples.ka

   1 ------------------------------------------------------------
   2 -- Naturals
   3
   4 data Nat : * => { zero : Nat | suc : Nat -> Nat }
   5
   6 one : Nat => (suc zero)
   7 two : Nat => (suc one)
   8 three : Nat => (suc two)
   9
  10 ------------------------------------------------------------
  11 -- Binary trees
  12
  13 data Tree : [A : *] -> * =>
  14   { leaf : Tree A | node : Tree A -> A -> Tree A -> Tree A }
  15
  16 ------------------------------------------------------------
  17 -- Empty types
  18
  19 data Empty : * => { }
  20
  21 ------------------------------------------------------------
  22 -- Ordered lists
  23
  24 record Unit : * => tt { }
  25
  26 le [n : Nat] : Nat -> * => (
  27   Nat-Elim
  28     n
  29     (\_ => Nat -> *)
  30     (\_ => Unit)
  31     (\n f m => Nat-Elim m (\_ => *) Empty (\m' _ => f m'))
  32 )
  33
  34 data Lift : * =>
  35   { bot : Lift | lift : Nat -> Lift | top : Lift }
  36
  37 le' [l1 : Lift] : Lift -> * => (
  38   Lift-Elim
  39     l1
  40     (\_ => Lift -> *)
  41     (\_     => Unit)
  42     (\n1 l2 => Lift-Elim l2 (\_ => *) Empty (\n2 => le n1 n2) Unit)
  43     (\l2    => Lift-Elim l2 (\_ => *) Empty (\_  => Empty)    Unit)
  44 )
  45
  46 data OList : [low upp : Lift] -> * =>
  47   { nil  : le' low upp -> OList low upp
  48   | cons : [n : Nat] -> OList (lift n) upp -> le' low (lift n) -> OList low upp
  49   }
  50
  51 ------------------------------------------------------------
  52 -- Dependent products
  53
  54 record Prod : [A : *] [B : A -> *] -> * =>
  55   prod {fst : A, snd : B fst}