score didn t change when changing the Import of Data.Nat.Show (#2025)

Author: Sofia-Insa

src/Data/Fin/Show.agda

@@ -11,7 +11,7 @@ module Data.Fin.Show where
 open import Data.Fin.Base using (Fin; toℕ; fromℕ<)
 open import Data.Maybe.Base using (Maybe; nothing; just; _>>=_)
 open import Data.Nat as ℕ using (ℕ; _≤?_; _<?_)
-import Data.Nat.Show as ℕ
+import Data.Nat.Show as ℕ using (show; readMaybe)
 open import Data.String.Base using (String)
 open import Function.Base
 open import Relation.Nullary.Decidable using (yes; no)

src/Data/Integer.agda

@@ -30,7 +30,7 @@ open import Data.Integer.Properties public
 -- Version 1.5
 -- Show
 
-import Data.Nat.Show as ℕ
+import Data.Nat.Show as ℕ using (show)
 open import Data.Sign as Sign using (Sign)
 open import Data.String.Base using (String; _++_)
 

src/System/Clock.agda

@@ -12,7 +12,7 @@ open import Level using (Level; 0ℓ; Lift; lower)
 open import Data.Bool.Base using (if_then_else_)
 open import Data.Fin.Base using (Fin; toℕ)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _∸_; _^_; _<ᵇ_)
-import Data.Nat.Show as ℕ
+import Data.Nat.Show as ℕ using (show)
 open import Data.Nat.DivMod using (_/_)
 import Data.Nat.Properties as ℕₚ
 open import Data.String.Base using (String; _++_; padLeft)

src/System/Console/ANSI.agda

@@ -10,7 +10,7 @@ module System.Console.ANSI where
 
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.Nat.Base using (ℕ; _+_)
-import Data.Nat.Show as ℕ
+import Data.Nat.Show as ℕ using (show)
 open import Data.String.Base using (String; concat; intersperse)
 open import Function.Base using (_$_; case_of_)
 

src/Test/Golden.agda

@@ -88,7 +88,7 @@ open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties using (infi
 open import Data.List.Relation.Unary.Any using (any?)
 open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
 open import Data.Nat.Base using (ℕ; _≡ᵇ_; _<ᵇ_; _+_; _∸_)
-import Data.Nat.Show as ℕ
+import Data.Nat.Show as ℕ using (show)
 open import Data.Product using (_×_; _,_)
 open import Data.String as String using (String; lines; unlines; unwords; concat; _≟_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)

src/Text/Printf.agda

@@ -14,7 +14,7 @@ open import Function.Base using (id)
 import Data.Char.Base    as Cₛ
 import Data.Integer.Show as ℤₛ
 import Data.Float        as Fₛ
-import Data.Nat.Show     as ℕₛ
+import Data.Nat.Show     as ℕₛ  using (show)
 
 open import Text.Format as Format hiding (Error)
 open import Text.Printf.Generic