1 files changed, 4 insertions, 1 deletions
diff --git a/DepType.idr b/DepType.idr
index 54ac7ad..f85a595 100644
--- a/DepType.idr
+++ b/DepType.idr
@@ -1,4 +1,6 @@
 module DepType
+  
+import Data.Fin
 
 isSingleton : Bool -> Type
 isSingleton True = Nat
@@ -16,4 +18,5 @@ data MyVect : Nat -> Type -> Type where
 (++) [] ys = ys
 (++) (x :: xs) ys = x :: xs ++ ys
 
--- The finite sets.
+length : MyVect n a -> Nat
+length xs {n} = n