Qualified import of Data.Nat fixing #2280 (#2281)

* `Algebra.Properties.Semiring.Binomial`

* `Codata.Sized.Cowriter`

* `Data.Char.Properties`

* `Data.Difference*`

* `Data.Fin.*`

* `Data.Float.Properties`

* `Data.Graph.Acyclic`

* `Data.Integer.Divisibility`: still need to disambiguate `Divisibility`?

* `Data.List.Extrema.Nat`

* `Data.List.Relation.Binary.*`

* `Data.Nat.Binary.*`

* `Data.Rational.Base`

* `Data.String`

* `Data.Vec.*`

* `Data.Word`

* `Induction.Lexicographic`

* `Reflection.AST`

* `Tactic.*`

* `Text.*`

Author: jamesmckinna

src/Algebra/Properties/Semiring/Binomial.agda

@@ -10,10 +10,10 @@
 
 open import Algebra.Bundles using (Semiring)
 open import Data.Bool.Base using (true)
-open import Data.Nat.Base as Nat hiding (_+_; _*_; _^_)
+open import Data.Nat.Base as ℕ hiding (_+_; _*_; _^_)
 open import Data.Nat.Combinatorics
   using (_C_; nCn≡1; nC1≡n; nCk+nC[k+1]≡[n+1]C[k+1])
-open import Data.Nat.Properties as Nat
+open import Data.Nat.Properties as ℕ
   using (<⇒<ᵇ; n<1+n; n∸n≡0; +-∸-assoc)
 open import Data.Fin.Base as Fin
   using (Fin; zero; suc; toℕ; fromℕ; inject₁)
@@ -154,8 +154,8 @@ y*lemma x*y≈y*x {n} j = begin
 -- Now, a lemma characterising the sum of the term₁ and term₂ expressions
 
 private
-  n<ᵇ1+n : ∀ n → (n Nat.<ᵇ suc n) ≡ true
-  n<ᵇ1+n n with true ← n Nat.<ᵇ suc n | _ ← <⇒<ᵇ (n<1+n n) = ≡.refl
+  n<ᵇ1+n : ∀ n → (n ℕ.<ᵇ suc n) ≡ true
+  n<ᵇ1+n n with true ← n ℕ.<ᵇ suc n | _ ← <⇒<ᵇ (n<1+n n) = ≡.refl
 
 term₁+term₂≈term : x * y ≈ y * x → ∀ n i → term₁ n i + term₂ n i ≈ binomialTerm (suc n) i
 
@@ -193,7 +193,7 @@ term₁+term₂≈term x*y≈y*x n (suc i) with view i
     ≈⟨ +-congˡ (×-congˡ nC[k+1]≡nC[j+1]) ⟨
   (nCk × [x^k+1]*[y^n-k]) + (nC[k+1] × [x^k+1]*[y^n-k])
     ≈⟨ ×-homo-+ [x^k+1]*[y^n-k] nCk nC[k+1] ⟨
-  (nCk Nat.+ nC[k+1]) × [x^k+1]*[y^n-k]
+  (nCk ℕ.+ nC[k+1]) × [x^k+1]*[y^n-k]
     ≡⟨ cong (_× [x^k+1]*[y^n-k]) (nCk+nC[k+1]≡[n+1]C[k+1] n k) ⟩
   ((suc n) C (suc k)) × [x^k+1]*[y^n-k]
     ≡⟨⟩

src/Codata/Sized/Cowriter.agda

@@ -17,7 +17,7 @@ open import Codata.Sized.Stream as Stream using (Stream; _∷_)
 open import Data.Unit.Base
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty.Base using (List⁺; _∷_)
-open import Data.Nat.Base as Nat using (ℕ; zero; suc)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Data.Product.Base as Prod using (_×_; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.Vec.Base using (Vec; []; _∷_)

src/Data/Char/Properties.agda

@@ -11,7 +11,7 @@ module Data.Char.Properties where
 open import Data.Bool.Base using (Bool)
 open import Data.Char.Base
 import Data.Nat.Base as ℕ
-import Data.Nat.Properties as ℕₚ
+import Data.Nat.Properties as ℕ
 open import Data.Product.Base using (_,_)
 
 open import Function.Base
@@ -56,7 +56,7 @@ open import Agda.Builtin.Char.Properties
 
 infix 4 _≟_
 _≟_ : Decidable {A = Char} _≡_
-x ≟ y = map′ ≈⇒≡ ≈-reflexive (toℕ x ℕₚ.≟ toℕ y)
+x ≟ y = map′ ≈⇒≡ ≈-reflexive (toℕ x ℕ.≟ toℕ y)
 
 setoid : Setoid _ _
 setoid = PropEq.setoid Char
@@ -95,22 +95,22 @@ private
 
 infix 4 _<?_
 _<?_ : Decidable _<_
-_<?_ = On.decidable toℕ ℕ._<_ ℕₚ._<?_
+_<?_ = On.decidable toℕ ℕ._<_ ℕ._<?_
 
 <-cmp : Trichotomous _≡_ _<_
-<-cmp c d with ℕₚ.<-cmp (toℕ c) (toℕ d)
+<-cmp c d with ℕ.<-cmp (toℕ c) (toℕ d)
 ... | tri< lt ¬eq ¬gt = tri< lt (≉⇒≢ ¬eq) ¬gt
 ... | tri≈ ¬lt eq ¬gt = tri≈ ¬lt (≈⇒≡ eq) ¬gt
 ... | tri> ¬lt ¬eq gt = tri> ¬lt (≉⇒≢ ¬eq) gt
 
 <-irrefl : Irreflexive _≡_ _<_
-<-irrefl = ℕₚ.<-irrefl ∘′ cong toℕ
+<-irrefl = ℕ.<-irrefl ∘′ cong toℕ
 
 <-trans : Transitive _<_
-<-trans {c} {d} {e} = On.transitive toℕ ℕ._<_ ℕₚ.<-trans {c} {d} {e}
+<-trans {c} {d} {e} = On.transitive toℕ ℕ._<_ ℕ.<-trans {c} {d} {e}
 
 <-asym : Asymmetric _<_
-<-asym {c} {d} = On.asymmetric toℕ ℕ._<_ ℕₚ.<-asym {c} {d}
+<-asym {c} {d} = On.asymmetric toℕ ℕ._<_ ℕ.<-asym {c} {d}
 
 <-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
 <-isStrictPartialOrder = record
@@ -151,7 +151,7 @@ _≤?_ = Reflₚ.decidable <-cmp
 ≤-trans = Reflₚ.trans (λ {a} {b} {c} → <-trans {a} {b} {c})
 
 ≤-antisym : Antisymmetric _≡_ _≤_
-≤-antisym = Reflₚ.antisym _≡_ refl ℕₚ.<-asym
+≤-antisym = Reflₚ.antisym _≡_ refl ℕ.<-asym
 
 ≤-isPreorder : IsPreorder _≡_ _≤_
 ≤-isPreorder = record
@@ -220,7 +220,7 @@ Please use Propositional Equality's subst instead."
 
 infix 4 _≈?_
 _≈?_ : Decidable _≈_
-x ≈? y = toℕ x ℕₚ.≟ toℕ y
+x ≈? y = toℕ x ℕ.≟ toℕ y
 
 ≈-isEquivalence : IsEquivalence _≈_
 ≈-isEquivalence = record
@@ -277,28 +277,28 @@ Please use decSetoid instead."
 #-}
 
 <-isStrictPartialOrder-≈ : IsStrictPartialOrder _≈_ _<_
-<-isStrictPartialOrder-≈ = On.isStrictPartialOrder toℕ ℕₚ.<-isStrictPartialOrder
+<-isStrictPartialOrder-≈ = On.isStrictPartialOrder toℕ ℕ.<-isStrictPartialOrder
 {-# WARNING_ON_USAGE <-isStrictPartialOrder-≈
 "Warning: <-isStrictPartialOrder-≈ was deprecated in v1.5.
 Please use <-isStrictPartialOrder instead."
 #-}
 
 <-isStrictTotalOrder-≈ : IsStrictTotalOrder _≈_ _<_
-<-isStrictTotalOrder-≈ = On.isStrictTotalOrder toℕ ℕₚ.<-isStrictTotalOrder
+<-isStrictTotalOrder-≈ = On.isStrictTotalOrder toℕ ℕ.<-isStrictTotalOrder
 {-# WARNING_ON_USAGE <-isStrictTotalOrder-≈
 "Warning: <-isStrictTotalOrder-≈ was deprecated in v1.5.
 Please use <-isStrictTotalOrder instead."
 #-}
 
 <-strictPartialOrder-≈ : StrictPartialOrder _ _ _
-<-strictPartialOrder-≈ = On.strictPartialOrder ℕₚ.<-strictPartialOrder toℕ
+<-strictPartialOrder-≈ = On.strictPartialOrder ℕ.<-strictPartialOrder toℕ
 {-# WARNING_ON_USAGE <-strictPartialOrder-≈
 "Warning: <-strictPartialOrder-≈ was deprecated in v1.5.
 Please use <-strictPartialOrder instead."
 #-}
 
 <-strictTotalOrder-≈ : StrictTotalOrder _ _ _
-<-strictTotalOrder-≈ = On.strictTotalOrder ℕₚ.<-strictTotalOrder toℕ
+<-strictTotalOrder-≈ = On.strictTotalOrder ℕ.<-strictTotalOrder toℕ
 {-# WARNING_ON_USAGE <-strictTotalOrder-≈
 "Warning: <-strictTotalOrder-≈ was deprecated in v1.5.
 Please use <-strictTotalOrder instead."

src/Data/DifferenceNat.agda

@@ -9,7 +9,7 @@
 
 module Data.DifferenceNat where
 
-open import Data.Nat.Base as N using (ℕ)
+open import Data.Nat.Base as ℕ using (ℕ)
 open import Function.Base using (_⟨_⟩_)
 
 infixl 6 _+_
@@ -21,7 +21,7 @@ Diffℕ = ℕ → ℕ
 0# = λ k → k
 
 suc : Diffℕ → Diffℕ
-suc n = λ k → N.suc (n k)
+suc n = λ k → ℕ.suc (n k)
 
 1# : Diffℕ
 1# = suc 0#
@@ -35,4 +35,4 @@ toℕ n = n 0
 -- fromℕ n is linear in the size of n.
 
 fromℕ : ℕ → Diffℕ
-fromℕ n = λ k → n ⟨ N._+_ ⟩ k
+fromℕ n = λ k → n ⟨ ℕ._+_ ⟩ k

src/Data/DifferenceVec.agda

@@ -9,9 +9,9 @@
 module Data.DifferenceVec where
 
 open import Data.DifferenceNat
-open import Data.Vec.Base as V using (Vec)
+open import Data.Vec.Base as Vec using (Vec)
 open import Function.Base using (_⟨_⟩_)
-import Data.Nat.Base as N
+import Data.Nat.Base as ℕ
 
 infixr 5 _∷_ _++_
 
@@ -22,7 +22,7 @@ DiffVec A m = ∀ {n} → Vec A n → Vec A (m n)
 [] = λ k → k
 
 _∷_ : ∀ {a} {A : Set a} {n} → A → DiffVec A n → DiffVec A (suc n)
-x ∷ xs = λ k → V._∷_ x (xs k)
+x ∷ xs = λ k → Vec._∷_ x (xs k)
 
 [_] : ∀ {a} {A : Set a} → A → DiffVec A 1#
 [ x ] = x ∷ []
@@ -32,25 +32,25 @@ _++_ : ∀ {a} {A : Set a} {m n} →
 xs ++ ys = λ k → xs (ys k)
 
 toVec : ∀ {a} {A : Set a} {n} → DiffVec A n → Vec A (toℕ n)
-toVec xs = xs V.[]
+toVec xs = xs Vec.[]
 
 -- fromVec xs is linear in the length of xs.
 
 fromVec : ∀ {a} {A : Set a} {n} → Vec A n → DiffVec A (fromℕ n)
-fromVec xs = λ k → xs ⟨ V._++_ ⟩ k
+fromVec xs = λ k → xs ⟨ Vec._++_ ⟩ k
 
 head : ∀ {a} {A : Set a} {n} → DiffVec A (suc n) → A
-head xs = V.head (toVec xs)
+head xs = Vec.head (toVec xs)
 
 tail : ∀ {a} {A : Set a} {n} → DiffVec A (suc n) → DiffVec A n
-tail xs = λ k → V.tail (xs k)
+tail xs = λ k → Vec.tail (xs k)
 
 take : ∀ {a} {A : Set a} m {n} →
        DiffVec A (fromℕ m + n) → DiffVec A (fromℕ m)
-take N.zero    xs = []
-take (N.suc m) xs = head xs ∷ take m (tail xs)
+take ℕ.zero    xs = []
+take (ℕ.suc m) xs = head xs ∷ take m (tail xs)
 
 drop : ∀ {a} {A : Set a} m {n} →
        DiffVec A (fromℕ m + n) → DiffVec A n
-drop N.zero    xs = xs
-drop (N.suc m) xs = drop m (tail xs)
+drop ℕ.zero    xs = xs
+drop (ℕ.suc m) xs = drop m (tail xs)

src/Data/Fin.agda

@@ -9,8 +9,7 @@
 module Data.Fin where
 
 open import Relation.Nullary.Decidable.Core
-open import Data.Nat.Base using (suc)
-import Data.Nat.Properties as ℕₚ
+import Data.Nat.Properties as ℕ
 
 ------------------------------------------------------------------------
 -- Publicly re-export the contents of the base module
@@ -27,5 +26,5 @@ open import Data.Fin.Properties public
 
 infix 10 #_
 
-#_ : ∀ m {n} {m<n : True (suc m ℕₚ.≤? n)} → Fin n
+#_ : ∀ m {n} {m<n : True (m ℕ.<? n)} → Fin n
 #_ _ {m<n = m<n} = fromℕ< (toWitness m<n)

src/Data/Fin/Permutation/Components.agda

@@ -12,7 +12,6 @@ open import Data.Bool.Base using (Bool; true; false)
 open import Data.Fin.Base
 open import Data.Fin.Properties
 open import Data.Nat.Base as ℕ using (zero; suc; _∸_)
-import Data.Nat.Properties as ℕₚ
 open import Data.Product.Base using (proj₂)
 open import Function.Base using (_∘_)
 open import Relation.Nullary.Reflects using (invert)