From e37fe01dbf5a9b12b880feeb54872e697e3a8bb1 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 17 Jan 2025 12:24:05 +0000 Subject: [PATCH] refactor: cosmetic, tighten `import`s --- src/Data/Nat/Primality/Factorisation.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 89b107ef26..b41eef323b 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -25,7 +25,7 @@ open import Data.List.Membership.Propositional.Properties using (∈-∃++) open import Data.List.Relation.Unary.All as All using (All; []; _∷_) open import Data.List.Relation.Unary.Any using (here; there) open import Data.List.Relation.Binary.Permutation.Propositional - using (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; refl; module PermutationReasoning) + using (_↭_; ↭-reflexive; ↭-refl; ↭-trans; module PermutationReasoning) open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (All-resp-↭; shift) open import Data.Sum.Base using (inj₁; inj₂) @@ -147,7 +147,7 @@ factorisationHasAllPrimeFactors {a ∷ as} {p} pPrime p∣aΠas (aPrime ∷ asPr private factorisationUnique′ : (as bs : List ℕ) → product as ≡ product bs → All Prime as → All Prime bs → as ↭ bs - factorisationUnique′ [] [] Πas≡Πbs asPrime bsPrime = refl + factorisationUnique′ [] [] Πas≡Πbs asPrime bsPrime = ↭-refl factorisationUnique′ [] (b@(2+ _) ∷ bs) Πas≡Πbs prime[as] (_ ∷ prime[bs]) = contradiction Πas≡Πbs (<⇒≢ Πas<Πbs) where