@@ -17,7 +17,7 @@ open import Data.Maybe.Base as Maybe using (Maybe; nothing; _<∣>_; when)
17
17
import Data.Maybe.Effectful as Maybe
18
18
open import Data.Nat
19
19
open import Data.Product using (proj₁)
20
- open import Data.String as String using (String)
20
+ open import Data.String.Base using (toList; fromList; String)
21
21
open import Function.Base
22
22
open import Relation.Nullary.Decidable using (True)
23
23
@@ -28,7 +28,7 @@ readMaybe : ∀ base {base≤16 : True (base ≤? 16)} → String → Maybe ℕ
28
28
readMaybe _ "" = nothing
29
29
readMaybe base = Maybe.map convert
30
30
∘′ TraversableA.mapA Maybe.applicative readDigit
31
- ∘′ String. toList
31
+ ∘′ toList
32
32
33
33
where
34
34
@@ -62,7 +62,7 @@ toDecimalChars : ℕ → List Char
62
62
toDecimalChars = List.map toDigitChar ∘′ toNatDigits 10
63
63
64
64
show : ℕ → String
65
- show = String. fromList ∘ toDecimalChars
65
+ show = fromList ∘ toDecimalChars
66
66
67
67
-- Arbitrary base betwen 2 & 16.
68
68
-- Warning: when compiled the time complexity of `showInBase b n` is
@@ -81,5 +81,5 @@ showInBase : (base : ℕ)
81
81
{base≥2 : True (2 ≤? base)}
82
82
{base≤16 : True (base ≤? 16 )} →
83
83
ℕ → String
84
- showInBase base {base≥2} {base≤16} = String. fromList
84
+ showInBase base {base≥2} {base≤16} = fromList
85
85
∘ charsInBase base {base≥2} {base≤16}
0 commit comments