Tidying up Data.String (#2061)

src/Data/String.agda

@@ -8,23 +8,17 @@
 
 module Data.String where
 
-open import Data.Bool using (true; false; T?)
+open import Data.Bool.Base using (if_then_else_)
 open import Data.Char as Char using (Char)
-open import Function.Base
-open import Data.Nat.Base as ℕ using (ℕ; _∸_; ⌊_/2⌋; ⌈_/2⌉)
+open import Function.Base using (_∘_; _$_)
+open import Data.Nat.Base as ℕ using (ℕ)
 import Data.Nat.Properties as ℕₚ
-open import Data.List.Base as List using (List; _∷_; []; [_])
-open import Data.List.NonEmpty as NE using (List⁺)
+open import Data.List.Base as List using (List)
 open import Data.List.Extrema ℕₚ.≤-totalOrder
-open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
-open import Data.List.Relation.Binary.Lex.Strict using (Lex-<; Lex-≤)
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.Char.Base as Char using (Char)
 import Data.Char.Properties as Char using (_≟_)
-open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-open import Relation.Nullary.Decidable using (does)
-open import Relation.Unary using (Pred; Decidable)
+open import Relation.Nullary.Decidable.Core using (does)
 
 open import Data.List.Membership.DecPropositional Char._≟_
 
@@ -48,9 +42,7 @@ fromVec = fromList ∘ Vec.toList
 
 -- enclose string with parens if it contains a space character
 parensIfSpace : String → String
-parensIfSpace s with does (' ' ∈? toList s)
-... | true = parens s
-... | false = s
+parensIfSpace s = if does (' ' ∈? toList s) then parens s else s
 
 
 ------------------------------------------------------------------------