blob: e0370cc5360573b86e1b69a59b9da7b4a2499cc5 (
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
|
------------------------------------------------------------
-- Naturals
data Nat : ⋆ ⇒ { zero : Nat | suc : Nat → Nat }
one : Nat ⇒ (suc zero)
two : Nat ⇒ (suc one)
three : Nat ⇒ (suc two)
------------------------------------------------------------
-- Binary trees
data Tree : [A : ⋆] → ⋆ ⇒
{ leaf : Tree A | node : Tree A → A → Tree A → Tree A }
------------------------------------------------------------
-- Empty types
data Empty : ⋆ ⇒ { }
------------------------------------------------------------
-- Ordered lists
record Unit : ⋆ ⇒ tt { }
le [n : Nat] : Nat → ⋆ ⇒ (
Nat-Elim
n
(λ _ ⇒ Nat → ⋆)
(λ _ ⇒ Unit)
(λ n f m ⇒ Nat-Elim m (λ _ ⇒ ⋆) Empty (λ m' _ ⇒ f m'))
)
data Lift : ⋆ ⇒
{ bot : Lift | lift : Nat → Lift | top : Lift }
le' [l1 : Lift] : Lift → ⋆ ⇒ (
Lift-Elim
l1
(λ _ ⇒ Lift → ⋆)
(λ _ ⇒ Unit)
(λ n1 l2 ⇒ Lift-Elim l2 (λ _ ⇒ ⋆) Empty (λ n2 ⇒ le n1 n2) Unit)
(λ l2 ⇒ Lift-Elim l2 (λ _ ⇒ ⋆) Empty (λ _ ⇒ Empty) Unit)
)
data OList : [low upp : Lift] → ⋆ ⇒
{ onil : le' low upp → OList low upp
| ocons : [n : Nat] → OList (lift n) upp → le' low (lift n) → OList low upp
}
data List : [A : ⋆] → ⋆ ⇒
{ nil : List A | cons : A → List A → List A }
------------------------------------------------------------
-- Dependent products
record Prod : [A : ⋆] [B : A → ⋆] → ⋆ ⇒
prod {fst : A, snd : B fst}
|