refactor: Bool analogue of agda#2558

Author: jamesmckinna

CHANGELOG.md

@@ -21,9 +21,19 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Data.List.Base`:
+  ```agda
+  and       ↦  Data.Bool.ListAction.and
+  or        ↦  Data.Bool.ListAction.or
+  any       ↦  Data.Bool.ListAction.any
+  all       ↦  Data.Bool.ListAction.all
+  ```
+
 New modules
 -----------
 
+* `Data.List.Base.{and|or|any|all}` and their properties have been lifted out into `Data.Bool.ListAction`.
+
 Additions to existing modules
 -----------------------------
 

src/Data/Bool/ListAction.agda

@@ -0,0 +1,39 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Natural numbers: sum and product of lists
+--
+-- Issue #2553: this is a compatibility stub module,
+-- ahead of a more thorough breaking set of changes.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Bool.ListAction where
+
+open import Data.Bool.Base using (Bool; _∧_; _∨_; true; false)
+open import Data.List.Base using (List; map; foldr)
+open import Function.Base using (_∘_)
+open import Level
+
+private
+  variable
+    a : Level
+    A : Set a
+
+
+------------------------------------------------------------------------
+-- Definitions
+
+and : List Bool → Bool
+and = foldr _∧_ true
+
+or : List Bool → Bool
+or = foldr _∨_ false
+
+any : (A → Bool) → List A → Bool
+any p = or ∘ map p
+
+all : (A → Bool) → List A → Bool
+all p = and ∘ map p
+

src/Data/List/Base.agda

@@ -16,7 +16,7 @@ open import Data.Bool.Base as Bool
   using (Bool; false; true; not; _∧_; _∨_; if_then_else_)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _*_ ; _≤_ ; s≤s)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Data.Product.Base as Product using (_×_; _,_; map₁; map₂′)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
@@ -150,24 +150,6 @@ null : List A → Bool
 null []       = true
 null (x ∷ xs) = false
 
-and : List Bool → Bool
-and = foldr _∧_ true
-
-or : List Bool → Bool
-or = foldr _∨_ false
-
-any : (A → Bool) → List A → Bool
-any p = or ∘ map p
-
-all : (A → Bool) → List A → Bool
-all p = and ∘ map p
-
-sum : List ℕ → ℕ
-sum = foldr _+_ 0
-
-product : List ℕ → ℕ
-product = foldr _*_ 1
-
 length : List A → ℕ
 length = foldr (const suc) 0
 
@@ -580,3 +562,33 @@ scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs
 "Warning: scanl was deprecated in v2.1.
 Please use Data.List.Scans.Base.scanl instead."
 #-}
+
+-- Version 2.3
+
+and : List Bool → Bool
+and = foldr _∧_ true
+
+all : (A → Bool) → List A → Bool
+all p = and ∘ map p
+{-# WARNING_ON_USAGE and
+"Warning: and was deprecated in v2.3.
+Please use Data.Bool.ListAction.and instead."
+#-}
+{-# WARNING_ON_USAGE all
+"Warning: all was deprecated in v2.3.
+Please use Data.Nat.ListAction.all instead."
+#-}
+
+or : List Bool → Bool
+or = foldr _∨_ false
+
+any : (A → Bool) → List A → Bool
+any p = or ∘ map p
+{-# WARNING_ON_USAGE or
+"Warning: or was deprecated in v2.3.
+Please use Data.Bool.ListAction.or instead."
+#-}
+{-# WARNING_ON_USAGE any
+"Warning: any was deprecated in v2.3.
+Please use Data.Bool.ListAction.any instead."
+#-}