Add map to Data.String.Base

CHANGELOG.md

@@ -80,3 +80,8 @@ Additions to existing modules
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
   ```
+
+* Added new functions in `Data.String.Base`:
+  ```agda
+  map : (Char → Char) → String → String
+  ```

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

src/Data/Tree/Rose/Show.agda

@@ -15,7 +15,7 @@ open import Data.DifferenceList as DList renaming (DiffList to DList) using ()
 open import Data.List.Base as List using (List; []; [_]; _∷_; _∷ʳ_)
 open import Data.Nat.Base using (ℕ; _∸_)
 open import Data.Product.Base using (_×_; _,_)
-open import Data.String.Base hiding (show)
+open import Data.String.Base using (String; _++_)
 open import Data.Tree.Rose using (Rose; node; map; fromBinary)
 open import Function.Base using (flip; _∘′_; id)
 

src/IO.agda

@@ -11,7 +11,7 @@ module IO where
 open import Codata.Musical.Notation
 open import Codata.Musical.Costring
 open import Data.Unit.Polymorphic.Base
-open import Data.String.Base
+open import Data.String.Base using (String)
 import Data.Unit.Base as Unit0
 open import Function.Base using (_∘_; flip)
 import IO.Primitive as Prim

src/Text/Printf/Generic.agda

@@ -15,7 +15,7 @@ open import Data.Maybe.Base hiding (map)
 open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base hiding (map)
 open import Data.Product.Nary.NonDependent
-open import Data.String.Base
+open import Data.String.Base using (String)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Unit.Base using (⊤)
 open import Function.Nary.NonDependent