demo.ka

   1 data Empty : * ⇒ {}
   2
   3 absurd [A : *] [x : Empty] : A ⇒ (
   4   Empty-Elim x (λ _ ⇒ A)
   5 )
   6
   7 record Unit : * ⇒ tt {}
   8
   9 data Nat : * ⇒ { zero : Nat | suc : Nat → Nat }
  10
  11 data List : [A : *] → * ⇒
  12   { nil : List A | cons : A → List A → List A }
  13
  14 nonEmpty [A : *] [l : List A] : * ⇒ (
  15    {| h1 |}
  16 )
  17
  18 nonEmpty [A : *] [l : List A] : * ⇒ (
  19   List-Elim l (λ _ ⇒ *) {|h1|} {|h2|}
  20 )
  21
  22 nonEmpty [A : *] [l : List A] : * ⇒ (
  23   List-Elim l (λ _ ⇒ *) Empty (λ _ _ _ ⇒ Unit)
  24 )
  25
  26 head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
  27   List-Elim l (λ l ⇒ nonEmpty A l → A)
  28     {|h1|} {|h2|}
  29 )
  30
  31 head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
  32   List-Elim l (λ l ⇒ nonEmpty A l → A)
  33    (λ p ⇒ {|h1 p|})
  34    (λ x l pl pxl ⇒ {|h2 x l pl pxl|})
  35 )
  36
  37 head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
  38   List-Elim l (λ l ⇒ nonEmpty A l → A)
  39     (λ p ⇒ absurd A p)
  40     (λ x l pl pxl ⇒ x)
  41 )