projects
/
bitonic-mengthesis.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
foo
[bitonic-mengthesis.git]
/
examples.ka
diff --git
a/examples.ka
b/examples.ka
index 072ab79e364772b077c66b03ec913ba53ab7db7c..cedf81a91ce79026172e159e4788727e77376949 100644
(file)
--- a/
examples.ka
+++ b/
examples.ka
@@
-44,10
+44,13
@@
le' [l1 : Lift] : Lift -> * => (
)
data OList : [low 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
+ {
o
nil : le' low upp -> OList low upp
+ |
o
cons : [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
------------------------------------------------------------
-- Dependent products