fixing agda#2280

Author: jamesmckinna

src/Data/Integer/Divisibility.agda

@@ -14,42 +14,40 @@ open import Function.Base using (_on_; _$_)
 open import Data.Integer.Base
 open import Data.Integer.Properties
 import Data.Nat.Base as ℕ
-import Data.Nat.Divisibility as ℕᵈ
+import Data.Nat.Divisibility as ℕ
 open import Level
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality
+
 
 ------------------------------------------------------------------------
 -- Divisibility
 
 infix 4 _∣_
 
 _∣_ : Rel ℤ 0ℓ
-_∣_ = ℕᵈ._∣_ on ∣_∣
-
-open ℕᵈ public using (divides)
+_∣_ = ℕ._∣_ on ∣_∣
 
 ------------------------------------------------------------------------
 -- Properties of divisibility
 
 *-monoʳ-∣ : ∀ k → (k *_) Preserves _∣_ ⟶ _∣_
 *-monoʳ-∣ k {i} {j} i∣j = begin
   ∣ k * i ∣       ≡⟨ abs-* k i ⟩
-  ∣ k ∣ ℕ.* ∣ i ∣ ∣⟨ ℕᵈ.*-monoʳ-∣ ∣ k ∣ i∣j ⟩
-  ∣ k ∣ ℕ.* ∣ j ∣ ≡⟨ sym (abs-* k j) ⟩
+  ∣ k ∣ ℕ.* ∣ i ∣ ∣⟨ ℕ.*-monoʳ-∣ ∣ k ∣ i∣j ⟩
+  ∣ k ∣ ℕ.* ∣ j ∣ ≡⟨ abs-* k j ⟨
   ∣ k * j ∣       ∎
-  where open ℕᵈ.∣-Reasoning
+  where open ℕ.∣-Reasoning
 
 *-monoˡ-∣ : ∀ k → (_* k) Preserves _∣_ ⟶ _∣_
 *-monoˡ-∣ k {i} {j} rewrite *-comm i k | *-comm j k = *-monoʳ-∣ k
 
 *-cancelˡ-∣ : ∀ k {i j} .{{_ : NonZero k}} → k * i ∣ k * j → i ∣ j
-*-cancelˡ-∣ k {i} {j} k*i∣k*j = ℕᵈ.*-cancelˡ-∣ ∣ k ∣ $ begin
-  ∣ k ∣ ℕ.* ∣ i ∣  ≡⟨ sym (abs-* k i) ⟩
+*-cancelˡ-∣ k {i} {j} k*i∣k*j = ℕ.*-cancelˡ-∣ ∣ k ∣ $ begin
+  ∣ k ∣ ℕ.* ∣ i ∣  ≡⟨ abs-* k i ⟨
   ∣ k * i ∣        ∣⟨ k*i∣k*j ⟩
   ∣ k * j ∣        ≡⟨ abs-* k j ⟩
   ∣ k ∣ ℕ.* ∣ j ∣  ∎
-  where open ℕᵈ.∣-Reasoning
+  where open ℕ.∣-Reasoning
 
 *-cancelʳ-∣ : ∀ k {i j} .{{_ : NonZero k}} → i * k ∣ j * k → i ∣ j
 *-cancelʳ-∣ k {i} {j} rewrite *-comm i k | *-comm j k = *-cancelˡ-∣ k

src/Data/Integer/Divisibility/Signed.agda

@@ -11,9 +11,7 @@ module Data.Integer.Divisibility.Signed where
 open import Function.Base using (_⟨_⟩_; _$_; _$′_; _∘_; _∘′_)
 open import Data.Integer.Base
 open import Data.Integer.Properties
-open import Data.Integer.Divisibility as Unsigned
-  using (divides)
-  renaming (_∣_ to _∣ᵤ_)
+import Data.Integer.Divisibility as Unsigned
 import Data.Nat.Base as ℕ
 import Data.Nat.Divisibility as ℕ
 import Data.Nat.Coprimality as ℕ
@@ -45,9 +43,9 @@ open _∣_ using (quotient) public
 ------------------------------------------------------------------------
 -- Conversion between signed and unsigned divisibility
 
-∣ᵤ⇒∣ : ∀ {k i} → k ∣ᵤ i → k ∣ i
-∣ᵤ⇒∣ {k} {i} (divides 0           eq) = divides (+ 0) (∣i∣≡0⇒i≡0 eq)
-∣ᵤ⇒∣ {k} {i} (divides q@(ℕ.suc _) eq) with k ≟ +0
+∣ᵤ⇒∣ : ∀ {k i} → k Unsigned.∣ i → k ∣ i
+∣ᵤ⇒∣ {k} {i} (ℕ.divides 0           eq) = divides (+ 0) (∣i∣≡0⇒i≡0 eq)
+∣ᵤ⇒∣ {k} {i} (ℕ.divides q@(ℕ.suc _) eq) with k ≟ +0
 ... | yes refl = divides +0 (∣i∣≡0⇒i≡0 (trans eq (ℕ.*-zeroʳ q)))
 ... | no  neq  = divides (sign i Sign.* sign k ◃ q) (◃-cong sign-eq abs-eq)
   where
@@ -85,8 +83,8 @@ open _∣_ using (quotient) public
     ∣ i ∣              ∎
     where open ≡-Reasoning
 
-∣⇒∣ᵤ : ∀ {k i} → k ∣ i → k ∣ᵤ i
-∣⇒∣ᵤ {k} {i} (divides q eq) = divides ∣ q ∣ $′ begin
+∣⇒∣ᵤ : ∀ {k i} → k ∣ i → k Unsigned.∣ i
+∣⇒∣ᵤ {k} {i} (divides q eq) = ℕ.divides ∣ q ∣ $′ begin
   ∣ i ∣           ≡⟨ cong ∣_∣ eq ⟩
   ∣ q * k ∣       ≡⟨ abs-* q k ⟩
   ∣ q ∣ ℕ.* ∣ k ∣ ∎

src/Data/Integer/GCD.agda

@@ -11,10 +11,9 @@ module Data.Integer.GCD where
 open import Data.Integer.Base
 open import Data.Integer.Divisibility
 open import Data.Integer.Properties
-open import Data.Nat.Base
 import Data.Nat.GCD as ℕ
 open import Data.Product.Base using (_,_)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
 open import Algebra.Definitions {A = ℤ} _≡_ as Algebra
   using (Associative; Commutative; LeftIdentity; RightIdentity; LeftZero; RightZero; Zero)

src/Data/Integer/LCM.agda

@@ -11,9 +11,8 @@ module Data.Integer.LCM where
 open import Data.Integer.Base
 open import Data.Integer.Divisibility
 open import Data.Integer.GCD
-open import Data.Nat.Base using (ℕ)
 import Data.Nat.LCM as ℕ
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
 ------------------------------------------------------------------------
 -- Definition