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)
70 two : Nat => (suc one)
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)