diff options
Diffstat (limited to 'examples.ka')
-rw-r--r-- | examples.ka | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/examples.ka b/examples.ka new file mode 100644 index 0000000..45e69e4 --- /dev/null +++ b/examples.ka @@ -0,0 +1,48 @@ +-- 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 : Lift] [upp : Lift] -> * => + { nil : le' low upp -> OList low upp + | cons : [n : Nat] -> OList (lift n) upp -> le' low (lift n) -> OList low upp + } + +-- Dependent products + +record Prod : [A : *] [B : A -> *] -> * => + prod {fst : A, snd : B fst} |