From e533c8b2885bbebea0b39de754e44d574ec37131 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 28 Feb 2025 07:40:40 +0000 Subject: [PATCH 1/3] fix: issue #2629 --- src/Algebra/Properties/Magma/Divisibility.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda index cbbc4cac70..1d38c29d42 100644 --- a/src/Algebra/Properties/Magma/Divisibility.agda +++ b/src/Algebra/Properties/Magma/Divisibility.agda @@ -39,7 +39,7 @@ x∣yx : ∀ x y → x ∣ y ∙ x x∣yx x y = y , refl xy≈z⇒y∣z : ∀ x y {z} → x ∙ y ≈ z → y ∣ z -xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x) +xy≈z⇒y∣z x y xy≈z = x , xy≈z ------------------------------------------------------------------------ -- Properties of non-divisibility From ae527d6f4e8a3e27f9bd01f65a6c91eeb397046f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 28 Feb 2025 07:41:42 +0000 Subject: [PATCH 2/3] fix: uncaught use of deprecated name --- src/Algebra/Properties/CommutativeMagma/Divisibility.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda b/src/Algebra/Properties/CommutativeMagma/Divisibility.agda index 9261d80e82..979476f5e0 100644 --- a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda +++ b/src/Algebra/Properties/CommutativeMagma/Divisibility.agda @@ -28,7 +28,7 @@ x∣xy : ∀ x y → x ∣ x ∙ y x∣xy x y = y , comm y x xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z -xy≈z⇒x∣z x y xy≈z = ∣-respʳ xy≈z (x∣xy x y) +xy≈z⇒x∣z x y xy≈z = {!∣-respʳ-≈ xy≈z (x∣xy x y)!} x|xy∧y|xy : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y) x|xy∧y|xy x y = x∣xy x y , x∣yx y x From fd75f501d6a25260c6410979d0b92f1ee32eae3d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 28 Feb 2025 07:49:05 +0000 Subject: [PATCH 3/3] check: possible knock opportunity --- src/Algebra/Properties/CommutativeMagma/Divisibility.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda b/src/Algebra/Properties/CommutativeMagma/Divisibility.agda index 979476f5e0..432f039203 100644 --- a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda +++ b/src/Algebra/Properties/CommutativeMagma/Divisibility.agda @@ -28,7 +28,7 @@ x∣xy : ∀ x y → x ∣ x ∙ y x∣xy x y = y , comm y x xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z -xy≈z⇒x∣z x y xy≈z = {!∣-respʳ-≈ xy≈z (x∣xy x y)!} +xy≈z⇒x∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣xy x y) x|xy∧y|xy : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y) x|xy∧y|xy x y = x∣xy x y , x∣yx y x