blob: cedf81a91ce79026172e159e4788727e77376949 (
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}
|
