From 0e437bd26a299b17aea9bd37d7fbacd9e9ae00fd Mon Sep 17 00:00:00 2001 From: Sofia-Insa Date: Thu, 13 Jul 2023 13:21:35 -0400 Subject: [PATCH] score didn t change when changing the Import of Data.Nat.Show --- src/Data/Fin/Show.agda | 2 +- src/Data/Integer.agda | 2 +- src/System/Clock.agda | 2 +- src/System/Console/ANSI.agda | 2 +- src/Test/Golden.agda | 2 +- src/Text/Printf.agda | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/Fin/Show.agda b/src/Data/Fin/Show.agda index 360cc8b1fc..8f9ae0583b 100644 --- a/src/Data/Fin/Show.agda +++ b/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 (ℕ; _≤?_; _