diff options
| author | Francesco Mazzoli <f@mazzo.li> | 2013-06-14 13:23:59 +0100 |
|---|---|---|
| committer | Francesco Mazzoli <f@mazzo.li> | 2013-06-14 13:23:59 +0100 |
| commit | ffa2d9635d358274433cece34fa326a49794ab62 (patch) | |
| tree | eb0d9c5073cfd19d1f0f601190a6e35c7473983a /examples.ka | |
| parent | fb4e0b4b2daac3838f6161836298cd4d1bf54766 (diff) | |
foo
Diffstat (limited to 'examples.ka')
| -rw-r--r-- | examples.ka | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/examples.ka b/examples.ka index 072ab79..cedf81a 100644 --- a/examples.ka +++ b/examples.ka @@ -44,10 +44,13 @@ le' [l1 : Lift] : 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 + { 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 |