@@ -52,3 +52,30 @@ mapElem : {xs : Vect k t} -> {f : t -> u} -> Elem x xs -> Elem (f x) (map f xs)
5252mapElem Here = Here
5353mapElem (There e) = There (mapElem e)
5454
55+-- Some convenience functions for testing lengths
56+
57+||| If the given Vect is the required length, return a Vect with that
58+||| length in its type, otherwise return Nothing
59+||| @len the required length
60+||| @xs the vector with the desired length
61+-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we
62+-- only know we don't know how to make a Vect n a, not that one can't exist.
63+isLength : {m : Nat} -> -- expected at run-time
64+ (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
65+isLength {m} len xs with (decEq m len)
66+ isLength {m = m} m xs | (Yes Refl) = Just xs
67+ isLength {m = m} len xs | (No contra) = Nothing
68+
69+||| If the given Vect is at least the required length, return a Vect with
70+||| at least that length in its type, otherwise return Nothing
71+||| @len the required length
72+||| @xs the vector with the desired length
73+overLength : {m : Nat} -> -- expected at run-time
74+ (len : Nat) -> (xs : Vect m a) -> Maybe (p ** Vect (plus p len) a)
75+overLength {m} n xs with (cmp m n)
76+ overLength {m = m} (plus m (S y)) xs | (CmpLT y) = Nothing
77+ overLength {m = m} m xs | CmpEQ
78+ = Just (0 ** xs)
79+ overLength {m = plus n (S x)} n xs | (CmpGT x)
80+ = Just (S x ** rewrite plusCommutative (S x) n in xs)
81+