diff options
Diffstat (limited to 'examples.ka')
| -rw-r--r-- | examples.ka | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/examples.ka b/examples.ka index 45e69e4..072ab79 100644 --- a/examples.ka +++ b/examples.ka @@ -1,3 +1,4 @@ +------------------------------------------------------------ -- Naturals data Nat : * => { zero : Nat | suc : Nat -> Nat } @@ -6,13 +7,18 @@ 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 { } @@ -37,11 +43,12 @@ le' [l1 : Lift] : Lift -> * => ( (\l2 => Lift-Elim l2 (\_ => *) Empty (\_ => Empty) Unit) ) -data OList : [low : Lift] [upp : Lift] -> * => +data OList : [low 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 -> *] -> * => |