refactor: fix deprecation problem

agda · Jan 17, 2025 · c1423d2 · c1423d2
1 parent e37fe01
commit c1423d2
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -400,13 +400,14 @@ mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f
 
 -- Version 2.3
 
-open import Data.Nat.SumAndProduct public
-  using (sum-↭; product-↭)
+import Data.Nat.SumAndProduct as ℕ
 
+sum-↭ = ℕ.sum-↭
 {-# WARNING_ON_USAGE sum-↭
 "Warning: sum-↭ was deprecated in v2.3.
 Please use Data.Nat.SumAndProduct.sum-↭ instead."
 #-}
+product-↭ = ℕ.product-↭
 {-# WARNING_ON_USAGE product-↭
 "Warning: product-↭ was deprecated in v2.3.
 Please use Data.Nat.SumAndProduct.product-↭ instead."