3 absurd [A : *] [x : Empty] : A ⇒ (
7 record Unit : * ⇒ tt {}
9 data Nat : * ⇒ { zero : Nat | suc : Nat → Nat }
11 data List : [A : *] → * ⇒
12 { nil : List A | cons : A → List A → List A }
14 nonEmpty [A : *] [l : List A] : * ⇒ (
18 nonEmpty [A : *] [l : List A] : * ⇒ (
19 List-Elim l (λ _ ⇒ *) {|h1|} {|h2|}
22 nonEmpty [A : *] [l : List A] : * ⇒ (
23 List-Elim l (λ _ ⇒ *) Empty (λ _ _ _ ⇒ Unit)
26 head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
27 List-Elim l (λ l ⇒ nonEmpty A l → A)
31 head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
32 List-Elim l (λ l ⇒ nonEmpty A l → A)
34 (λ x l pl pxl ⇒ {|h2 x l pl pxl|})
37 head [A : *] [l : List A] : nonEmpty A l → A ⇒ (
38 List-Elim l (λ l ⇒ nonEmpty A l → A)