Skip to content

Commit

Permalink
Get rid of redundant dependencies in System.Console.ANSI (#1994)
Browse files Browse the repository at this point in the history
  • Loading branch information
Saransh-cpp authored and andreasabel committed Jul 10, 2024
1 parent 0376427 commit 662374e
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/Data/Nat/Show.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand All @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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}

0 comments on commit 662374e

Please sign in to comment.