From dd85bc115f0b27e6caaae84a3ce4ec4be65ec02b Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Fri, 16 Jun 2023 18:25:02 -0400 Subject: [PATCH 1/2] Get rid of redundant deps in `System.Console.ANSI` redundant deps : `Function.HalfAdjointEquivalence` `Data.Product.Function.Dependent.Propositional` replaced `Data.String` import with `Data.String.Base` in `Data.Nat.Show` --- 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..4acd910d9a 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 hiding (show) 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} From 76af6b6dd97b5e1bfc78439188de46e0eab856f4 Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Fri, 16 Jun 2023 19:10:02 -0400 Subject: [PATCH 2/2] Readability --- src/Algebra/Definitions.agda | 2 +- src/Data/Nat/Show.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index c0820fafb7..e64fc4f30b 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -109,7 +109,7 @@ _DistributesOver_ : Op₂ A → Op₂ A → Set _ * DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +) _MiddleFourExchange_ : Op₂ A → Op₂ A → Set _ -_*_ MiddleFourExchange _+_ = +_*_ MiddleFourExchange _+_ = ∀ w x y z → ((w + x) * (y + z)) ≈ ((w + y) * (x + z)) _IdempotentOn_ : Op₂ A → A → Set _ diff --git a/src/Data/Nat/Show.agda b/src/Data/Nat/Show.agda index 4acd910d9a..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.Base hiding (show) +open import Data.String.Base using (toList; fromList; String) open import Function.Base open import Relation.Nullary.Decidable using (True)