projects
/
bitonic-mengthesis.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
more report
[bitonic-mengthesis.git]
/
examples.ka
diff --git
a/examples.ka
b/examples.ka
index 45e69e4cb1a2dcf1832e1f54b5e5e37d6c4f14fb..072ab79e364772b077c66b03ec913ba53ab7db7c 100644
(file)
--- a/
examples.ka
+++ b/
examples.ka
@@
-1,3
+1,4
@@
+------------------------------------------------------------
-- Naturals
data Nat : * => { zero : Nat | suc : Nat -> Nat }
-- Naturals
data Nat : * => { zero : Nat | suc : Nat -> Nat }
@@
-6,13
+7,18
@@
one : Nat => (suc zero)
two : Nat => (suc one)
three : Nat => (suc two)
two : Nat => (suc one)
three : Nat => (suc two)
+------------------------------------------------------------
-- Binary trees
-- Binary trees
+
data Tree : [A : *] -> * =>
{ leaf : Tree A | node : Tree A -> A -> Tree A -> Tree A }
data Tree : [A : *] -> * =>
{ leaf : Tree A | node : Tree A -> A -> Tree A -> Tree A }
+------------------------------------------------------------
-- Empty types
-- Empty types
+
data Empty : * => { }
data Empty : * => { }
+------------------------------------------------------------
-- Ordered lists
record Unit : * => tt { }
-- Ordered lists
record Unit : * => tt { }
@@
-37,11
+43,12
@@
le' [l1 : Lift] : Lift -> * => (
(\l2 => Lift-Elim l2 (\_ => *) Empty (\_ => Empty) Unit)
)
(\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
}
{ 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 -> *] -> * =>
-- Dependent products
record Prod : [A : *] [B : A -> *] -> * =>