Skip to content

Commit c1423d2

Browse files
committed
refactor: fix deprecation problem
1 parent e37fe01 commit c1423d2

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -400,13 +400,14 @@ mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f
400400

401401
-- Version 2.3
402402

403-
open import Data.Nat.SumAndProduct public
404-
using (sum-↭; product-↭)
403+
import Data.Nat.SumAndProduct as ℕ
405404

405+
sum-↭ = ℕ.sum-↭
406406
{-# WARNING_ON_USAGE sum-↭
407407
"Warning: sum-↭ was deprecated in v2.3.
408408
Please use Data.Nat.SumAndProduct.sum-↭ instead."
409409
#-}
410+
product-↭ = ℕ.product-↭
410411
{-# WARNING_ON_USAGE product-↭
411412
"Warning: product-↭ was deprecated in v2.3.
412413
Please use Data.Nat.SumAndProduct.product-↭ instead."

0 commit comments

Comments
 (0)