From 5fdff3ce532f7373b5fb6bd3f9b663ad4b79e158 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Wed, 17 Apr 2024 22:48:59 -0400 Subject: [PATCH 1/2] Closes #2315 --- CHANGELOG.md | 6 ++++++ src/Algebra/Structures.agda | 4 ++++ 2 files changed, 10 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 469c926af8..e55fc3ad94 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -249,6 +249,12 @@ Additions to existing modules x \\ y = (x ⁻¹) ∙ y ``` +* In `Algebra.Structures.IsCancellativeCommutativeSemiring` add the + extra property as an exposed definition: + ```agda + *-cancelʳ-nonZero : AlmostRightCancellative 0# * + ``` + * In `Data.Container.Indexed.Core`: ```agda Subtrees o c = (r : Response c) → X (next c r) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 066363686f..6a30c51dde 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -573,6 +573,10 @@ record IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a open IsCommutativeSemiring isCommutativeSemiring public + *-cancelʳ-nonZero : AlmostRightCancellative 0# * + *-cancelʳ-nonZero = Consequences.comm∧almostCancelˡ⇒almostCancelʳ setoid + *-comm *-cancelˡ-nonZero + record IsIdempotentSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where field isSemiring : IsSemiring + * 0# 1# From 8c0ff683c1a1d9dabf5da1f14fdcc208cd7dc517 Mon Sep 17 00:00:00 2001 From: Jacques Carette Date: Wed, 17 Apr 2024 22:53:07 -0400 Subject: [PATCH 2/2] whitespace --- src/Algebra/Structures.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index 6a30c51dde..3cdc55a4b5 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -576,7 +576,7 @@ record IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a *-cancelʳ-nonZero : AlmostRightCancellative 0# * *-cancelʳ-nonZero = Consequences.comm∧almostCancelˡ⇒almostCancelʳ setoid *-comm *-cancelˡ-nonZero - + record IsIdempotentSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where field isSemiring : IsSemiring + * 0# 1#