@@ -17,7 +17,7 @@ open import Data.Maybe.Base as Maybe using (Maybe; nothing; _<∣>_; when)
1717import Data.Maybe.Effectful as Maybe
1818open import Data.Nat
1919open import Data.Product using (proj₁)
20- open import Data.String as String using (String)
20+ open import Data.String.Base using (toList; fromList; String)
2121open import Function.Base
2222open import Relation.Nullary.Decidable using (True)
2323
@@ -28,7 +28,7 @@ readMaybe : ∀ base {base≤16 : True (base ≤? 16)} → String → Maybe ℕ
2828readMaybe _ "" = nothing
2929readMaybe base = Maybe.map convert
3030 ∘′ TraversableA.mapA Maybe.applicative readDigit
31- ∘′ String. toList
31+ ∘′ toList
3232
3333 where
3434
@@ -62,7 +62,7 @@ toDecimalChars : ℕ → List Char
6262toDecimalChars = List.map toDigitChar ∘′ toNatDigits 10
6363
6464show : ℕ → String
65- show = String. fromList ∘ toDecimalChars
65+ show = fromList ∘ toDecimalChars
6666
6767-- Arbitrary base betwen 2 & 16.
6868-- Warning: when compiled the time complexity of `showInBase b n` is
@@ -81,5 +81,5 @@ showInBase : (base : ℕ)
8181 {base≥2 : True (2 ≤? base)}
8282 {base≤16 : True (base ≤? 16 )} →
8383 ℕ → String
84- showInBase base {base≥2} {base≤16} = String. fromList
84+ showInBase base {base≥2} {base≤16} = fromList
8585 ∘ charsInBase base {base≥2} {base≤16}
0 commit comments