Add map to Data.String.Base

CHANGELOG.md

@@ -3117,6 +3117,7 @@ Additions to existing modules
   ```agda
   wordsByᵇ : (Char → Bool) → String → List String
   linesByᵇ : (Char → Bool) → String → List String
+  map      : (Char → Char) → String → String
   ```
 
 * Added new proofs in `Data.String.Properties`:

src/Data/String/Base.agda

@@ -185,3 +185,9 @@ lines = linesByᵇ ('\n' Char.≈ᵇ_)
 -- `lines` preserves empty lines
 _ : lines "\nabc\n\nb\n\n\n" ≡ "" ∷ "abc" ∷ "" ∷ "b" ∷ "" ∷ "" ∷ []
 _ = refl
+
+map : (Char → Char) → String → String
+map f = fromList ∘ List.map f ∘ toList
+
+_ : map Char.toUpper "abc" ≡ "ABC"
+_ = refl