Remove showPrec, use show everywhere
This commit is contained in:
parent
989197d488
commit
5103fc0996
|
@ -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
|
||||
|
||||
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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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 _/_
|
||||
|
||||
|
|
Loading…
Reference in New Issue
Block a user