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   { onil  : le' low upp → OList low upp
  48   | ocons : [n : Nat] → OList (lift n) upp → le' low (lift n) → OList low upp
  49   }
  50
  51 data List : [A : ⋆] → ⋆ ⇒
  52   { nil : List A | cons : A → List A → List A }
  53
  54 ------------------------------------------------------------
  55 -- Dependent products
  56
  57 record Prod : [A : ⋆] [B : A → ⋆] → ⋆ ⇒
  58   prod {fst : A, snd : B fst}