diff --git a/Class/Show/Instances.agda b/Class/Show/Instances.agda index a747554..e3e59bc 100644 --- a/Class/Show/Instances.agda +++ b/Class/Show/Instances.agda @@ -29,6 +29,9 @@ instance Show-ℤ = Show _ ∋ record {M} where import Data.Integer.Show as M + Show-ℚ = Show _ ∋ record {M} + where import Data.Rational.Show as M + Show-Fin : Show¹ Fin Show-Fin .show = ("# " ◇_) ∘ show ∘ toℕ where open import Data.Fin using (toℕ)