@@ -614,11 +614,11 @@ mapElem (There e) = There (mapElem e)
614||| @xs the vector with the desired length
614||| @xs the vector with the desired length
615-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we
615-- Needs to be Maybe rather than Dec, because if 'n' is unequal to m, we
616-- only know we don't know how to make a Vect n a, not that one can't exist.
616-- only know we don't know how to make a Vect n a, not that one can't exist.
617−isLength : {m : Nat} -> -- expected at run-time
617+exactLength : {m : Nat} -> -- expected at run-time
618− (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
618+ (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)
619−isLength {m} len xs with (decEq m len)
619+exactLength {m} len xs with (decEq m len)
620− isLength {m = m} m xs | (Yes Refl) = Just xs
620+ exactLength {m = m} m xs | (Yes Refl) = Just xs
621− isLength {m = m} len xs | (No contra) = Nothing
621+ exactLength {m = m} len xs | (No contra) = Nothing
623||| If the given Vect is at least the required length, return a Vect with
623||| If the given Vect is at least the required length, return a Vect with
624||| at least that length in its type, otherwise return Nothing
624||| at least that length in its type, otherwise return Nothing