1 ------------------------------------------------------------
4 data Nat : * => { zero : Nat | suc : Nat -> Nat }
6 one : Nat => (suc zero)
8 three : Nat => (suc two)
10 ------------------------------------------------------------
13 data Tree : [A : *] -> * =>
14 { leaf : Tree A | node : Tree A -> A -> Tree A -> Tree A }
16 ------------------------------------------------------------
21 ------------------------------------------------------------
24 record Unit : * => tt { }
26 le [n : Nat] : Nat -> * => (
31 (\n f m => Nat-Elim m (\_ => *) Empty (\m' _ => f m'))
35 { bot : Lift | lift : Nat -> Lift | top : Lift }
37 le' [l1 : Lift] : Lift -> * => (
42 (\n1 l2 => Lift-Elim l2 (\_ => *) Empty (\n2 => le n1 n2) Unit)
43 (\l2 => Lift-Elim l2 (\_ => *) Empty (\_ => Empty) Unit)
46 data OList : [low upp : Lift] -> * =>
47 { onil : le' low upp -> OList low upp
48 | ocons : [n : Nat] -> OList (lift n) upp -> le' low (lift n) -> OList low upp
51 data List : [A : *] -> * =>
52 { nil : List A | cons : A -> List A -> List A }
54 ------------------------------------------------------------
57 record Prod : [A : *] [B : A -> *] -> * =>
58 prod {fst : A, snd : B fst}