diff --git a/src/Base.agda b/src/Base.agda index 4b8f19f..3378e8a 100644 --- a/src/Base.agda +++ b/src/Base.agda @@ -72,24 +72,23 @@ instance record Show (T : Type) : Type₁ where field - showPrec : T → ℕ → String.String - show : T → String.String - show x = showPrec x 0 + show : T → String.String + open Show ⦃...⦄ public instance open import Data.Nat.Show using () renaming (show to show-ℕ) ShowNat : Show ℕ - ShowNat .showPrec x _ = show-ℕ x + ShowNat .show x = show-ℕ x ShowString : Show String.String - ShowString .showPrec x _ = String.show x + ShowString .show x = String.show x ShowList : {A : Type} → ⦃ Show A ⦄ → Show (List A) - ShowList {A} .showPrec x _ = "[" String.++ go x String.++ "]" + ShowList {A} .show x = "[" String.++ go x String.++ "]" where go : List A → String.String go [] = "" - go (x ∷ []) = showPrec x 0 - go (x ∷ xs) = showPrec x 0 String.++ ", " String.++ go xs + go (x ∷ []) = show x + go (x ∷ xs) = show x String.++ ", " String.++ go xs diff --git a/src/Bits-and-Bytes.agda b/src/Bits-and-Bytes.agda index 8c9a2ba..dda854e 100644 --- a/src/Bits-and-Bytes.agda +++ b/src/Bits-and-Bytes.agda @@ -38,7 +38,7 @@ instance EqByte ._==_ a b = a .value == b .value ShowByte : Show Byte - ShowByte .showPrec x _ = "< " String.++ showPrec (x .value) 1 String.++ " >" + ShowByte .show x = "< " String.++ show (x .value) String.++ " >" where import Data.String as String diff --git a/src/NonEmpty.agda b/src/NonEmpty.agda index f772d83..d58c5b6 100644 --- a/src/NonEmpty.agda +++ b/src/NonEmpty.agda @@ -25,6 +25,6 @@ list⁺-to-list (x ∷⁺ xs) = x ∷ list⁺-to-list xs instance ShowList⁺ : {A : Type} → ⦃ Show A ⦄ → Show (List⁺ A) - ShowList⁺ .showPrec x p = showPrec (list⁺-to-list x) p String.++ "⁺" + ShowList⁺ .show x = show (list⁺-to-list x) String.++ "⁺" where import Data.String as String diff --git a/src/Parse-HTTP.agda b/src/Parse-HTTP.agda index 03cb498..07eaed2 100644 --- a/src/Parse-HTTP.agda +++ b/src/Parse-HTTP.agda @@ -29,7 +29,7 @@ data HTTP-Method : Type where instance ShowMethod : Show HTTP-Method - ShowMethod .showPrec x _ = go x + ShowMethod .show x = go x where go : HTTP-Method → String.String go GET = "GET" @@ -90,9 +90,9 @@ module Parse-URL where instance ShowPath : Show Path - ShowPath .showPrec $ _ = "(empty path)" - ShowPath .showPrec (p / $) _ = p - ShowPath .showPrec (p / rest@(_ / _)) n = p String.++ "/" String.++ showPrec rest n + ShowPath .show $ = "(empty path)" + ShowPath .show (p / $) = p + ShowPath .show (p / rest@(_ / _)) = p String.++ "/" String.++ show rest infixr 5 _/_