Add function to reduce All into Vec (#1263)

Author: umazalakain

CHANGELOG.md

@@ -497,6 +497,11 @@ Other minor additions
   transpose : ∀ {m n} → Vector (Vector A n) m → Vector (Vector A m) n
   ```
 
+* Added new functions to `Data.Vec.Relation.Unary.All`:
+  ```agda
+  reduce : (f : ∀ {x} → P x → B) → All P xs → Vec B n
+  ```
+
 * Added new proofs to `Data.Vec.Relation.Unary.All.Properties`:
   ```agda
   All-swap : ∀ {xs ys} → All (λ x → All (x ~_) ys) xs → All (λ y → All (_~ y) xs) ys

src/Data/Vec/Relation/Unary/All.agda

@@ -47,6 +47,10 @@ module _ {P : Pred A p} where
   tail : ∀ {n x} {xs : Vec A n} → All P (x ∷ xs) → All P xs
   tail (px ∷ pxs) = pxs
 
+  reduce : (f : ∀ {x} → P x → B) → ∀ {n} {xs : Vec A n} → All P xs → Vec B n
+  reduce f []         = []
+  reduce f (px ∷ pxs) = f px ∷ reduce f pxs
+
   uncons : ∀ {n x} {xs : Vec A n} → All P (x ∷ xs) → P x × All P xs
   uncons = < head , tail >