refactor: renamed new module

Author: jamesmckinna

CHANGELOG.md

@@ -23,28 +23,28 @@ Deprecated names
 
 * In `Data.List.Base`:
   ```agda
-  sum       ↦  Data.Nat.SumAndProduct.sum
-  product   ↦  Data.Nat.SumAndProduct.product
+  sum       ↦  Data.Nat.ListAction.sum
+  product   ↦  Data.Nat.ListAction.product
   ```
 
 * In `Data.List.Properties`:
   ```agda
-  sum-++       ↦  Data.Nat.SumAndProduct.sum-++
-  ∈⇒∣product   ↦  Data.Nat.SumAndProduct.∈⇒∣product
-  product≢0    ↦  Data.Nat.SumAndProduct.product≢0
-  ∈⇒≤product   ↦  Data.Nat.SumAndProduct.∈⇒≤product
+  sum-++       ↦  Data.Nat.ListAction.sum-++
+  ∈⇒∣product   ↦  Data.Nat.ListAction.∈⇒∣product
+  product≢0    ↦  Data.Nat.ListAction.product≢0
+  ∈⇒≤product   ↦  Data.Nat.ListAction.∈⇒≤product
   ```
 
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
   ```agda
-  sum-↭       ↦  Data.Nat.SumAndProduct.sum-↭
-  product-↭   ↦  Data.Nat.SumAndProduct.product-↭
+  sum-↭       ↦  Data.Nat.ListAction.sum-↭
+  product-↭   ↦  Data.Nat.ListAction.product-↭
   ```
 
 New modules
 -----------
 
-* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.SumAndProduct`.
+* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction`.
 
 Additions to existing modules
 -----------------------------

doc/README/Data/List.agda

@@ -7,7 +7,7 @@
 module README.Data.List where
 
 open import Data.Nat.Base using (ℕ; _+_)
-open import Data.Nat.SumAndProduct using (sum)
+open import Data.Nat.ListAction using (sum)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
 ------------------------------------------------------------------------

src/Data/List/Base.agda

@@ -581,13 +581,13 @@ sum : List ℕ → ℕ
 sum = foldr ℕ._+_ 0
 {-# WARNING_ON_USAGE sum
 "Warning: sum was deprecated in v2.3.
-Please use Data.Nat.SumAndProduct.sum instead."
+Please use Data.Nat.ListAction.sum instead."
 #-}
 
 product : List ℕ → ℕ
 product = foldr ℕ._*_ 1
 {-# WARNING_ON_USAGE product
 "Warning: product was deprecated in v2.3.
-Please use Data.Nat.SumAndProduct.product instead."
+Please use Data.Nat.ListAction.product instead."
 #-}
 

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

@@ -400,15 +400,15 @@ mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f
 
 -- Version 2.3
 
-import Data.Nat.SumAndProduct as ℕ
+import Data.Nat.ListAction as ℕ
 
 sum-↭ = ℕ.sum-↭
 {-# WARNING_ON_USAGE sum-↭
 "Warning: sum-↭ was deprecated in v2.3.
-Please use Data.Nat.SumAndProduct.sum-↭ instead."
+Please use Data.Nat.ListAction.sum-↭ instead."
 #-}
 product-↭ = ℕ.product-↭
 {-# WARNING_ON_USAGE product-↭
 "Warning: product-↭ was deprecated in v2.3.
-Please use Data.Nat.SumAndProduct.product-↭ instead."
+Please use Data.Nat.ListAction.product-↭ instead."
 #-}

src/Data/Nat/SumAndProduct.agda renamed to src/Data/Nat/ListAction.agda

@@ -9,7 +9,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-module Data.Nat.SumAndProduct where
+module Data.Nat.ListAction where
 
 open import Algebra.Bundles using (CommutativeMonoid)
 open import Data.List.Base using (List; []; _∷_; _++_; foldr)

src/Data/Nat/Primality.agda

@@ -14,7 +14,7 @@ open import Data.Nat.Base
 open import Data.Nat.Divisibility
 open import Data.Nat.GCD using (module GCD; module Bézout)
 open import Data.Nat.Properties
-open import Data.Nat.SumAndProduct using (product; product≢0)
+open import Data.Nat.ListAction using (product; product≢0)
 open import Data.Product.Base using (∃-syntax; _×_; map₂; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (flip; _∘_; _∘′_)

src/Data/Nat/Primality/Factorisation.agda

@@ -17,7 +17,7 @@ open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder)
 open import Data.Nat.Primality
   using (Prime; _Rough_; rough∧square>⇒prime; ∤⇒rough-suc; rough∧∣⇒rough; rough∧∣⇒prime;
          2-rough; euclidsLemma; prime⇒irreducible; ¬prime[1]; productOfPrimes≥1; prime⇒nonZero)
-open import Data.Nat.SumAndProduct using (product; product-↭)
+open import Data.Nat.ListAction using (product; product-↭)
 open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₁; proj₂)
 open import Data.List.Base using (List; []; _∷_; _++_)
 open import Data.List.Membership.Propositional using (_∈_)

src/Data/Tree/Binary/Zipper.agda

@@ -13,7 +13,7 @@ open import Data.Tree.Binary as BT using (Tree; node; leaf)
 open import Data.List.Base as List using (List; []; _∷_; _++_; [_])
 open import Data.Maybe.Base using (Maybe; nothing; just)
 open import Data.Nat.Base using (ℕ; suc; _+_)
-open import Data.Nat.SumAndProduct using (sum)
+open import Data.Nat.ListAction using (sum)
 open import Function.Base using (_$_; _∘_)
 
 private

src/Data/Tree/Binary/Zipper/Properties.agda

@@ -13,7 +13,7 @@ open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.All using (All; just; nothing)
 open import Data.Nat.Base using (ℕ; suc; _+_)
 open import Data.Nat.Properties using (+-identityʳ; +-comm; +-assoc)
-open import Data.Nat.SumAndProduct using (sum)
+open import Data.Nat.ListAction using (sum)
 open import Data.Tree.Binary as BT using (Tree; node; leaf)
 open import Data.Tree.Binary.Zipper using (Zipper; toTree; up; mkZipper;
   leftBranch; rightBranch; left; right; #nodes; Crumb; getTree; #leaves;

src/Test/Golden.agda

@@ -88,7 +88,7 @@ open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties using (infi
 open import Data.List.Relation.Unary.Any using (any?)
 open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe)
 open import Data.Nat.Base using (ℕ; _≡ᵇ_; _<ᵇ_; _+_; _∸_)
-open import Data.Nat.SumAndProduct using (sum)
+open import Data.Nat.ListAction using (sum)
 import Data.Nat.Show as ℕ using (show)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.String.Base as String using (String; lines; unlines; unwords; concat)