1 files changed, 19 insertions, 0 deletions
diff --git a/DepType.idr b/DepType.idr
new file mode 100644
index 0000000..54ac7ad
--- /dev/null
+++ b/DepType.idr
@@ -0,0 +1,19 @@
+module DepType
+
+isSingleton : Bool -> Type
+isSingleton True = Nat
+isSingleton False = List Nat
+  
+sum : (single : Bool) -> isSingleton single -> Nat
+sum True x = x
+sum False (x :: xs) = x + sum False xs
+
+data MyVect : Nat -> Type -> Type where
+  Nil : MyVect Z a
+  (::) : a -> MyVect k a -> MyVect (S k) a
+
+(++) : MyVect k a -> MyVect l a -> MyVect (k + l) a
+(++) [] ys = ys
+(++) (x :: xs) ys = x :: xs ++ ys
+
+-- The finite sets.