Skip to content

refine import of Data.Nat.Show #2025

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jul 28, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/Data/Fin/Show.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Integer.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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; _++_)

Expand Down
2 changes: 1 addition & 1 deletion src/System/Clock.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
2 changes: 1 addition & 1 deletion src/System/Console/ANSI.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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_)

Expand Down
2 changes: 1 addition & 1 deletion src/Test/Golden.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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₂)
Expand Down
2 changes: 1 addition & 1 deletion src/Text/Printf.agda
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down