1 ------------------------------------------------------------
6 absurd [A : ⋆] [x : Empty] : A ⇒ (
10 neg [A : ⋆] : ⋆ ⇒ (A → Empty)
12 record Unit : ⋆ ⇒ tt { }
14 record Prod : [A : ⋆] [B : A → ⋆] → ⋆ ⇒
15 prod {fst : A, snd : B fst}
17 data Bool : ⋆ ⇒ { true : Bool | false : Bool }
19 -- The if_then_else_ is provided by Bool-Elim
21 -- A large eliminator, for convenience
22 ITE [b : Bool] [A B : ⋆] : ⋆ ⇒ (
23 Bool-Elim b (λ _ ⇒ ⋆) A B
26 ------------------------------------------------------------
29 data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }
31 gt [n : Nat] : Nat → ⋆ ⇒ (
36 (λ n f m ⇒ Nat-Elim m (λ _ ⇒ ⋆) Unit (λ m' _ ⇒ f m'))
39 data List : [A : ⋆] → ⋆ ⇒
40 { nil : List A | cons : A → List A → List A }
42 length [A : ⋆] [xs : List A] : Nat ⇒ (
43 List-Elim xs (λ _ ⇒ Nat) zero (λ _ _ n ⇒ suc n)
46 head [A : ⋆] [xs : List A] : gt (length A xs) zero → A ⇒ (
49 (λ xs ⇒ gt (length A xs) zero → A)
54 ------------------------------------------------------------
57 data Parity : ⋆ ⇒ { even : Parity | odd : Parity }
59 flip [p : Parity] : Parity ⇒ (
60 Parity-Elim p (λ _ ⇒ Parity) odd even
63 parity [n : Nat] : Parity ⇒ (
64 Nat-Elim n (λ _ ⇒ Parity) even (λ _ ⇒ flip)
67 even [n : Nat] : ⋆ ⇒ (Parity-Elim (parity n) (λ _ ⇒ ⋆) Unit Empty)
69 one : Nat ⇒ (suc zero)
71 three : Nat ⇒ (suc two)
72 four : Nat ⇒ (suc three)
73 five : Nat ⇒ (suc four)
74 six : Nat ⇒ (suc five)
76 even-6 : even six ⇒ tt
78 even-5-neg : neg (even five) ⇒ (λ z ⇒ z)
80 there-is-an-even-number : Prod Nat even ⇒ (prod six even-6)
82 Or [A B : ⋆] : ⋆ ⇒ (Prod Bool (λ b ⇒ ITE b A B))
84 left [A B : ⋆] [x : A] : Or A B ⇒ (prod true x)
85 right [A B : ⋆] [x : B] : Or A B ⇒ (prod false x)
87 case [A B C : ⋆] [f : A → C] [g : B → C] [x : Or A B] : C ⇒ (
88 (Bool-Elim (fst x) (λ b ⇒ ITE b A B → C) f g) (snd x)