From 662374e3777a850d1a87f0fadb5a98d8645e807c Mon Sep 17 00:00:00 2001
From: Saransh Chopra <saransh0701@gmail.com>
Date: Sun, 18 Jun 2023 21:28:56 -0400
Subject: [PATCH] Get rid of redundant dependencies in `System.Console.ANSI`
 (#1994)

---
 src/Data/Nat/Show.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/Nat/Show.agda b/src/Data/Nat/Show.agda
index 454bc95b76..9f0fdf2bb5 100644
--- a/src/Data/Nat/Show.agda
+++ b/src/Data/Nat/Show.agda
@@ -17,7 +17,7 @@ open import Data.Maybe.Base as Maybe using (Maybe; nothing; _<∣>_; when)
 import Data.Maybe.Effectful as Maybe
 open import Data.Nat
 open import Data.Product using (proj₁)
-open import Data.String as String using (String)
+open import Data.String.Base using (toList; fromList; String)
 open import Function.Base
 open import Relation.Nullary.Decidable using (True)
 
@@ -28,7 +28,7 @@ readMaybe : ∀ base {base≤16 : True (base ≤? 16)} → String → Maybe ℕ
 readMaybe _ "" = nothing
 readMaybe base = Maybe.map convert
               ∘′ TraversableA.mapA Maybe.applicative readDigit
-              ∘′ String.toList
+              ∘′ toList
 
   where
 
@@ -62,7 +62,7 @@ toDecimalChars : ℕ → List Char
 toDecimalChars = List.map toDigitChar ∘′ toNatDigits 10
 
 show : ℕ → String
-show = String.fromList ∘ toDecimalChars
+show = fromList ∘ toDecimalChars
 
 -- Arbitrary base betwen 2 & 16.
 -- Warning: when compiled the time complexity of `showInBase b n` is
@@ -81,5 +81,5 @@ showInBase : (base : ℕ)
              {base≥2 : True (2 ≤? base)}
              {base≤16 : True (base ≤? 16)} →
              ℕ → String
-showInBase base {base≥2} {base≤16} = String.fromList
+showInBase base {base≥2} {base≤16} = fromList
                                    ∘ charsInBase base {base≥2} {base≤16}