diff --git a/CHANGELOG.md b/CHANGELOG.md index bf2d01d6a3..8a3ccbdae8 100644 --- a/CHANGELOG.md +++ b/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 + ``` diff --git a/src/Data/String/Base.agda b/src/Data/String/Base.agda index d583da042c..fb0ebc1526 100644 --- a/src/Data/String/Base.agda +++ b/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 diff --git a/src/Data/Tree/Rose/Show.agda b/src/Data/Tree/Rose/Show.agda index 5b293aeb70..1aa0509aae 100644 --- a/src/Data/Tree/Rose/Show.agda +++ b/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) diff --git a/src/IO.agda b/src/IO.agda index eebb5d7d92..96f7db2760 100644 --- a/src/IO.agda +++ b/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 diff --git a/src/Text/Printf/Generic.agda b/src/Text/Printf/Generic.agda index 07c8856443..21aa36133a 100644 --- a/src/Text/Printf/Generic.agda +++ b/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