Simplified String imports (#2016)

README/Data/List/Relation/Binary/Subset.agda

@@ -21,7 +21,8 @@ module README.Data.List.Relation.Binary.Subset where
 -- tell Agda which equality relation to use.
 
 -- Decidable equality over Strings
-open import Data.String using (String; _≟_)
+open import Data.String.Base using (String)
+open import Data.String.Properties using (_≟_)
 
 -- Open the decidable membership module using Decidable ≡ over Strings
 open import Data.List.Membership.DecPropositional _≟_

README/Data/Tree/AVL.agda

@@ -21,7 +21,7 @@ import Data.Tree.AVL
 
 open import Data.Nat.Properties using (<-strictTotalOrder)
 open import Data.Product as Prod using (_,_; _,′_)
-open import Data.String using (String)
+open import Data.String.Base using (String)
 open import Data.Vec using (Vec; _∷_; [])
 open import Relation.Binary.PropositionalEquality
 

README/Data/Trie/NonDependent.agda

@@ -57,7 +57,8 @@ open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Fresh as List# using (List#; []; _∷#_)
 open import Data.Maybe as Maybe
 open import Data.Product as Prod
-open import Data.String as String using (String)
+open import Data.String.Base as String using (String)
+open import Data.String.Properties as String using (_≟_)
 open import Data.These as These
 
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)

README/Function/Reasoning.agda

@@ -35,7 +35,8 @@ module _ {A B C : Set} {A→B : A → B} {B→C : B → C} where
 open import Data.Nat
 open import Data.List.Base
 open import Data.Char.Base
-open import Data.String as String using (String; toList; fromList; _==_)
+open import Data.String.Base as String using (String; toList; fromList)
+open import Data.String.Properties as String using (_==_)
 open import Function.Base using (_∘_)
 open import Data.Bool hiding (_≤?_)
 open import Data.Product as P using (_×_; <_,_>; uncurry; proj₁)

README/IO.agda

@@ -11,7 +11,7 @@ module README.IO where
 open import Level
 open import Data.Nat.Base
 open import Data.Nat.Show using (show)
-open import Data.String using (String; _++_; lines)
+open import Data.String.Base using (String; _++_; lines)
 open import Data.Unit.Polymorphic
 open import IO
 

src/Data/Rational.agda

@@ -26,7 +26,7 @@ open import Data.Rational.Properties public
 -- Version 1.5
 
 import Data.Integer.Show as ℤ
-open import Data.String using (String; _++_)
+open import Data.String.Base using (String; _++_)
 
 show : ℚ → String
 show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)

src/Reflection/AST/Abstraction.agda

@@ -8,8 +8,9 @@
 
 module Reflection.AST.Abstraction where
 
+open import Data.String.Base as String using (String)
+open import Data.String.Properties as String using (_≟_)
 open import Data.Product.Base using (_×_; <_,_>; uncurry)
-open import Data.String as String using (String)
 open import Level
 open import Relation.Nullary.Decidable using (Dec; map′; _×-dec_)
 open import Relation.Binary using (DecidableEquality)

src/Reflection/AST/Literal.agda

@@ -12,7 +12,7 @@ open import Data.Bool.Base using (Bool; true; false)
 import Data.Char as Char using (_≟_)
 import Data.Float as Float using (_≟_)
 import Data.Nat as ℕ using (_≟_)
-import Data.String as String using (_≟_)
+import Data.String.Properties as String using (_≟_)
 import Data.Word as Word using (_≟_)
 import Reflection.AST.Meta as Meta
 import Reflection.AST.Name as Name

src/Reflection/AST/Show.agda

@@ -15,9 +15,9 @@ import Data.Char as Char using (show)
 import Data.Float as Float using (show)
 open import Data.List.Base hiding (_++_; intersperse)
 import Data.Nat.Show as ℕ using (show)
+open import Data.String.Base as String using (String; _++_; intersperse; braces; parens; _<+>_)
+open import Data.String as String using (parensIfSpace)
 open import Data.Product.Base using (_×_; _,_)
-open import Data.String as String
- using (String; _++_; intersperse; braces; parens; parensIfSpace; _<+>_)
 import Data.Word as Word using (toℕ)
 open import Function.Base using (id; _∘′_; case_of_)
 open import Relation.Nullary.Decidable using (yes; no)

src/Reflection/AST/Term.agda

@@ -14,7 +14,8 @@ open import Data.Nat as ℕ using (ℕ; zero; suc)
 open import Data.Product.Base using (_×_; _,_; <_,_>; uncurry; map₁)
 open import Data.Product.Properties using (,-injective)
 open import Data.Maybe.Base using (Maybe; just; nothing)
-open import Data.String as String using (String)
+open import Data.String.Base using (String)
+open import Data.String.Properties as String hiding (_≟_)
 open import Relation.Nullary.Decidable using (map′; _×-dec_; yes; no)
 open import Relation.Binary using (Decidable; DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)

src/Reflection/AST/Traversal.agda

@@ -13,8 +13,8 @@ module Reflection.AST.Traversal
 
 open import Data.Nat using (ℕ; zero; suc; _+_)
 open import Data.List.Base using (List; []; _∷_; _++_; reverse; length)
+open import Data.String.Base using (String)
 open import Data.Product.Base using (_×_; _,_)
-open import Data.String using (String)
 open import Function.Base using (_∘_)
 open import Reflection hiding (pure)
 

src/Test/Golden.agda

@@ -90,7 +90,8 @@ open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
 open import Data.Nat.Base using (ℕ; _≡ᵇ_; _<ᵇ_; _+_; _∸_)
 import Data.Nat.Show as ℕ using (show)
 open import Data.Product.Base using (_×_; _,_)
-open import Data.String as String using (String; lines; unlines; unwords; concat; _≟_)
+open import Data.String.Base as String using (String; lines; unlines; unwords; concat)
+open import Data.String.Properties as String using (_≟_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Unit.Base using (⊤)
 

src/Text/Tabular/List.agda

@@ -8,7 +8,7 @@
 
 module Text.Tabular.List where
 
-open import Data.String using (String)
+open import Data.String.Base using (String)
 open import Data.List.Base
 import Data.Nat.Properties as ℕₚ
 open import Data.Product.Base using (-,_; proj₂)