diff options
| author | Francesco Mazzoli <f@mazzo.li> | 2013-06-11 01:14:23 +0100 |
|---|---|---|
| committer | Francesco Mazzoli <f@mazzo.li> | 2013-06-11 01:14:23 +0100 |
| commit | 1e1c98d47c6a32611f37b5d6da1060c5a09f268c (patch) | |
| tree | 96bce00ced934b252008f16c4cdf1e39f61aacaf /examples.ka | |
| parent | 798a3023430d620ec17004b4d9d68235bed97e28 (diff) | |
more report
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 -> *] -> * => |