From adc32aa717a1a5d759cb0f79eae199783b12a049 Mon Sep 17 00:00:00 2001 From: = Date: Tue, 6 Jul 2021 11:49:14 +0800 Subject: [PATCH] Stop `Data.Rational.Base` exporting `+0` and `+[1+_]` --- CHANGELOG.md | 4 ++++ src/Data/Rational/Base.agda | 9 +-------- src/Data/Rational/Properties.agda | 2 +- 3 files changed, 6 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 98e0f50fcd..5230681d7c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -53,6 +53,10 @@ Non-backwards compatible changes So `[a-zA-Z]+.agdai?` run on "the path _build/Main.agdai corresponds to" will return "Main.agdai" when it used to be happy to just return "n.agda". +* The constructors `+0` and `+[1+_]` from `Data.Integer.Base` are no longer + exported by `Data.Rational.Base`. You will have to open `Data.Integer(.Base)` + directly to use them. + Deprecated modules ------------------ diff --git a/src/Data/Rational/Base.agda b/src/Data/Rational/Base.agda index 55a0bf5f2d..b34ef95460 100644 --- a/src/Data/Rational/Base.agda +++ b/src/Data/Rational/Base.agda @@ -10,7 +10,7 @@ module Data.Rational.Base where open import Data.Bool.Base using (Bool; true; false; if_then_else_) open import Function.Base using (id) -open import Data.Integer.Base as ℤ using (ℤ; +_; +0; -[1+_]) +open import Data.Integer.Base as ℤ using (ℤ; +_; +0; +[1+_]; -[1+_]) import Data.Integer.GCD as ℤ import Data.Integer.DivMod as ℤ open import Data.Nat.GCD @@ -35,13 +35,6 @@ open import Relation.Binary.PropositionalEquality open ≡-Reasoning --- Note, these are re-exported publicly to maintain backwards --- compatability. Although we are unable (?) to put a warning on them, --- using these from `Data.Rational` should be viewed as a deprecated --- feature. - -open import Data.Integer public using (+0; +[1+_]) - ------------------------------------------------------------------------ -- Rational numbers in reduced form. Note that there is exactly one -- way to represent every rational number. diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index a7efd40e83..152faaf57d 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -20,7 +20,7 @@ import Algebra.Morphism.RingMonomorphism as RingMonomorphisms import Algebra.Morphism.LatticeMonomorphism as LatticeMonomorphisms import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties open import Data.Bool.Base using (T; true; false) -open import Data.Integer.Base as ℤ using (ℤ; +_; -[1+_]; 0ℤ; 1ℤ; _◃_) +open import Data.Integer.Base as ℤ using (ℤ; +_; -[1+_]; +[1+_]; +0; 0ℤ; 1ℤ; _◃_) open import Data.Integer.Coprimality using (coprime-divisor) import Data.Integer.Properties as ℤ open import Data.Integer.GCD using (gcd; gcd[i,j]≡0⇒i≡0; gcd[i,j]≡0⇒j≡0)