examples.ka

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