From 62b5bf26e97904397f36ad6be77ef2531a445df2 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 24 Oct 2022 15:19:22 +0100 Subject: [PATCH 1/5] [fix] issue #1844 --- src/Data/Integer/Properties.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index fa313d91f0..2c00eb38d4 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -944,8 +944,8 @@ distribʳ-⊖-+-neg m n o = begin ; ⁻¹-cong = cong (-_) } -+-isAbelianGroup : IsAbelianGroup _+_ +0 (-_) -+-isAbelianGroup = record ++-0-isAbelianGroup : IsAbelianGroup _+_ +0 (-_) ++-0-isAbelianGroup = record { isGroup = +-0-isGroup ; comm = +-comm } @@ -980,7 +980,7 @@ distribʳ-⊖-+-neg m n o = begin +-0-abelianGroup : AbelianGroup 0ℓ 0ℓ +-0-abelianGroup = record - { isAbelianGroup = +-isAbelianGroup + { isAbelianGroup = +-0-isAbelianGroup } ------------------------------------------------------------------------ @@ -1522,7 +1522,7 @@ private +-*-isRing : IsRing _+_ _*_ -_ 0ℤ 1ℤ +-*-isRing = record - { +-isAbelianGroup = +-isAbelianGroup + { +-isAbelianGroup = +-0-isAbelianGroup ; *-cong = cong₂ _*_ ; *-assoc = *-assoc ; *-identity = *-identity From 900f0873a4d89516a709034b95d68ab7e33e71f4 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 24 Oct 2022 18:25:43 +0100 Subject: [PATCH 2/5] [fix] issue #1755 for `Data.Integer` --- src/Data/Integer/Base.agda | 48 ++++++++++++++++++++++++++++++++ src/Data/Integer/Properties.agda | 6 ---- 2 files changed, 48 insertions(+), 6 deletions(-) diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda index 8b81cddd29..4432615c77 100644 --- a/src/Data/Integer/Base.agda +++ b/src/Data/Integer/Base.agda @@ -11,6 +11,8 @@ module Data.Integer.Base where +open import Algebra.Bundles.Raw + using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing) open import Data.Bool.Base using (Bool; T; true; false) open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s) open import Data.Sign.Base as Sign using (Sign) @@ -293,3 +295,49 @@ _%ℕ_ : (dividend : ℤ) (divisor : ℕ) .{{_ : ℕ.NonZero divisor}} → ℕ _%_ : (dividend divisor : ℤ) .{{_ : NonZero divisor}} → ℕ i % j = i %ℕ ∣ j ∣ + +------------------------------------------------------------------------ +-- Bundles + ++-rawMagma : RawMagma 0ℓ 0ℓ ++-rawMagma = record { _≈_ = _≡_ ; _∙_ = _+_ } + ++-0-rawMonoid : RawMonoid 0ℓ 0ℓ ++-0-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _+_ ; ε = 0ℤ } + +*-rawMagma : RawMagma 0ℓ 0ℓ +*-rawMagma = record { _≈_ = _≡_ ; _∙_ = _*_ } + +*-1-rawMonoid : RawMonoid 0ℓ 0ℓ +*-1-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _*_ ; ε = 1ℤ } + ++-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ ++-*-rawNearSemiring = record + { Carrier = _ + ; _≈_ = _≡_ + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = 0ℤ + } + ++-*-rawSemiring : RawSemiring 0ℓ 0ℓ ++-*-rawSemiring = record + { Carrier = _ + ; _≈_ = _≡_ + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = 0ℤ + ; 1# = 1ℤ + } + ++-*-rawRing : RawRing 0ℓ 0ℓ ++-*-rawRing = record + { Carrier = _ + ; _≈_ = _≡_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0ℤ + ; 1# = 1ℤ + } + diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 2c00eb38d4..53a3367245 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -1539,12 +1539,6 @@ private ------------------------------------------------------------------------ -- Bundles -*-rawMagma : RawMagma 0ℓ 0ℓ -*-rawMagma = record { _≈_ = _≡_ ; _∙_ = _*_ } - -*-1-rawMonoid : RawMonoid 0ℓ 0ℓ -*-1-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _*_ ; ε = 1ℤ } - *-magma : Magma 0ℓ 0ℓ *-magma = record { isMagma = *-isMagma From 14d46d4de9a6fbdfb7cf86de486c97c4dfb3bb2f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 25 Oct 2022 09:57:48 +0100 Subject: [PATCH 3/5] deprecation warning and `CHANGELOG` entry --- CHANGELOG.md | 2 ++ src/Data/Integer/Properties.agda | 5 +++++ 2 files changed, 7 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 02014e8d9f..c1132b227c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -946,6 +946,8 @@ Deprecated names pos-distrib-* ↦ pos-* pos-+-commute ↦ pos-+ abs-*-commute ↦ abs-* + + +-isAbelianGroup ↦ +-0-isAbelianGroup ``` * In `Data.List.Properties`: diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 53a3367245..80b8922e61 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -2381,3 +2381,8 @@ pos-distrib-* m n = sym (pos-* m n) "Warning: pos-distrib-* was deprecated in v2.0 Please use pos-* instead." #-} ++-isAbelianGroup = +-0-isAbelianGroup +{-# WARNING_ON_USAGE +-isAbelianGroup +"Warning: +-isAbelianGroup was deprecated in v2.0 +Please use +-0-isAbelianGroup instead." +#-} From 766755eaf1932dd6c69b63e9bf7dc29d3cfed217 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 25 Oct 2022 10:02:59 +0100 Subject: [PATCH 4/5] [fix] issues #1755 and #1865 --- src/Data/Integer/Properties.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 80b8922e61..cf0bf967a4 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -2386,3 +2386,6 @@ Please use pos-* instead." "Warning: +-isAbelianGroup was deprecated in v2.0 Please use +-0-isAbelianGroup instead." #-} +{- issue1844/issue1755: raw bundles have moved to `Data.X.Base` -} +open Data.Integer.Base public + using (*-rawMagma; *-1-rawMonoid) From 29e3844e139cff1cb05b39ad8895f0d6994204c5 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 25 Oct 2022 10:07:24 +0100 Subject: [PATCH 5/5] [fix] whitespace --- src/Data/Integer/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index cf0bf967a4..812347aea4 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -2387,5 +2387,5 @@ Please use pos-* instead." Please use +-0-isAbelianGroup instead." #-} {- issue1844/issue1755: raw bundles have moved to `Data.X.Base` -} -open Data.Integer.Base public +open Data.Integer.Base public using (*-rawMagma; *-1-rawMonoid)