added new function take-all to stdl

CHANGELOG.md

@@ -2053,6 +2053,8 @@ Other minor changes
 
   length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
   length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
+
+  take-all : n ≥ length l → take n xs ≡ xs     
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:

src/Data/List/Properties.agda

@@ -758,6 +758,13 @@ length-take zero    xs       = refl
 length-take (suc n) []       = refl
 length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)
 
+-- If you take at least as many elements from a list as it has, you get the whole list.
+take-all :(n : ℕ) (xs : List A) → n ≥ length xs → take n xs ≡ xs
+take-all zero [] _ = refl
+take-all (suc _) [] _ = refl
+take-all (suc n) (x ∷ xs) (s≤s pf) = cong (x ∷_) (take-all n xs pf)
+
+
 ------------------------------------------------------------------------
 -- drop