blob: 9545a557fe2645b846c5a13fa4d2874860942b9f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
------------------------------------------------------------
-- Core ITT (minus W)
data Empty : ⋆ ⇒ { }
absurd [A : ⋆] [x : Empty] : A ⇒ (
Empty-Elim x (λ _ ⇒ A)
)
neg [A : ⋆] : ⋆ ⇒ (A → Empty)
record Unit : ⋆ ⇒ tt { }
record Prod : [A : ⋆] [B : A → ⋆] → ⋆ ⇒
prod {fst : A, snd : B fst}
data Bool : ⋆ ⇒ { true : Bool | false : Bool }
-- The if_then_else_ is provided by Bool-Elim
-- A large eliminator, for convenience
ITE [b : Bool] [A B : ⋆] : ⋆ ⇒ (
Bool-Elim b (λ _ ⇒ ⋆) A B
)
------------------------------------------------------------
-- Examples →
data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }
gt [n : Nat] : Nat → ⋆ ⇒ (
Nat-Elim
n
(λ _ ⇒ Nat → ⋆)
(λ _ ⇒ Empty)
(λ n f m ⇒ Nat-Elim m (λ _ ⇒ ⋆) Unit (λ m' _ ⇒ f m'))
)
data List : [A : ⋆] → ⋆ ⇒
{ nil : List A | cons : A → List A → List A }
length [A : ⋆] [xs : List A] : Nat ⇒ (
List-Elim xs (λ _ ⇒ Nat) zero (λ _ _ n ⇒ suc n)
)
head [A : ⋆] [xs : List A] : gt (length A xs) zero → A ⇒ (
List-Elim
xs
(λ xs ⇒ gt (length A xs) zero → A)
(λ p ⇒ absurd A p)
(λ x _ _ _ ⇒ x)
)
------------------------------------------------------------
-- Examples ×
data Parity : ⋆ ⇒ { even : Parity | odd : Parity }
flip [p : Parity] : Parity ⇒ (
Parity-Elim p (λ _ ⇒ Parity) odd even
)
parity [n : Nat] : Parity ⇒ (
Nat-Elim n (λ _ ⇒ Parity) even (λ _ ⇒ flip)
)
even [n : Nat] : ⋆ ⇒ (Parity-Elim (parity n) (λ _ ⇒ ⋆) Unit Empty)
one : Nat ⇒ (suc zero)
two : Nat ⇒ (suc one)
three : Nat ⇒ (suc two)
four : Nat ⇒ (suc three)
five : Nat ⇒ (suc four)
six : Nat ⇒ (suc five)
even-6 : even six ⇒ tt
even-5-neg : neg (even five) ⇒ (λ z ⇒ z)
there-is-an-even-number : Prod Nat even ⇒ (prod six even-6)
Or [A B : ⋆] : ⋆ ⇒ (Prod Bool (λ b ⇒ ITE b A B))
left [A B : ⋆] [x : A] : Or A B ⇒ (prod true x)
right [A B : ⋆] [x : B] : Or A B ⇒ (prod false x)
case [A B C : ⋆] [f : A → C] [g : B → C] [x : Or A B] : C ⇒ (
(Bool-Elim (fst x) (λ b ⇒ ITE b A B → C) f g) (snd x)
)
|
