From 9aed9a7879eb378e2d0acf670e0f521d778eece6 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 16 Jan 2024 12:22:13 +0000
Subject: [PATCH 01/14] a better `scanr`

---
 CHANGELOG.md                     | 11 +++++++++++
 src/Data/List/Base.agda          | 19 +++++++++++++------
 src/Data/List/NonEmpty/Base.agda |  9 +++++++++
 3 files changed, 33 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5b3079dee4..f96c9951a1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,6 +21,11 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Data.List.Base`:
+  ```agda
+  scanr  : (A → B → B) → B → List A → List B
+  ```
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
@@ -37,6 +42,12 @@ Additions to existing modules
   nonZeroIndex : Fin n → ℕ.NonZero n
   ```
 
+* In `Data.List.NonEmpty.Base`:
+  ```agda
+  scanr⁺ : (A → B → B) → B → List A → List⁺ B
+  scanr  : (A → B → B) → B → List A → List B
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 16546110b6..6435289ac3 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -210,12 +210,6 @@ updateAt (x ∷ xs) (suc i) f = x ∷ updateAt xs i f
 
 -- Scans
 
-scanr : (A → B → B) → B → List A → List B
-scanr f e []       = e ∷ []
-scanr f e (x ∷ xs) with scanr f e xs
-... | []     = []                -- dead branch
-... | y ∷ ys = f x y ∷ y ∷ ys
-
 scanl : (A → B → A) → A → List B → List A
 scanl f e []       = e ∷ []
 scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs
@@ -570,3 +564,16 @@ _─_ = removeAt
 "Warning: _─_ was deprecated in v2.0.
 Please use removeAt instead."
 #-}
+
+-- Version 2.1
+
+scanr : (A → B → B) → B → List A → List B
+scanr f e []       = e ∷ []
+scanr f e (x ∷ xs) with scanr f e xs
+... | []     = []                -- dead branch
+... | y ∷ ys = f x y ∷ y ∷ ys
+{-# WARNING_ON_USAGE scanr
+"Warning: scanr was deprecated in v2.1.
+Please use List.NonEmpty.base.scanr instead."
+#-}
+
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index 82f16c270a..63379cfa56 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -121,6 +121,15 @@ foldl c s (x ∷ xs) = List.foldl c (s x) xs
 foldl₁ : (A → A → A) → List⁺ A → A
 foldl₁ f = foldl f id
 
+scanr⁺ : (A → B → B) → B → List A → List⁺ B
+scanr⁺ {A = A} {B = B} f e xs = go xs where
+  go : List A → List⁺ B
+  go []       = e ∷ []
+  go (x ∷ xs) = let y ∷ ys = go xs in f x y ∷ y ∷ ys
+
+scanr  : (A → B → B) → B → List A → List B
+scanr f e xs = toList (scanr⁺ f e xs)
+
 -- Append (several variants).
 
 infixr 5 _⁺++⁺_ _++⁺_ _⁺++_

From 370e69ccdb217620ac69b9dce62a068622cedc29 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 16 Jan 2024 12:40:53 +0000
Subject: [PATCH 02/14] typo in deprecation warning

---
 src/Data/List/Base.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 6435289ac3..4590d81b3b 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -574,6 +574,6 @@ scanr f e (x ∷ xs) with scanr f e xs
 ... | y ∷ ys = f x y ∷ y ∷ ys
 {-# WARNING_ON_USAGE scanr
 "Warning: scanr was deprecated in v2.1.
-Please use List.NonEmpty.base.scanr instead."
+Please use List.NonEmpty.Base.scanr instead."
 #-}
 

From 0ec35d093d79fb90ab15707cd6f3ff18b407404a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 16 Jan 2024 14:54:18 +0000
Subject: [PATCH 03/14] fixed `Properties`

---
 CHANGELOG.md                           | 10 +++++++++
 src/Data/List/NonEmpty/Base.agda       |  2 +-
 src/Data/List/NonEmpty/Properties.agda | 10 +++++++++
 src/Data/List/Properties.agda          | 29 +++++++++++++++-----------
 4 files changed, 38 insertions(+), 13 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f96c9951a1..46ea38d263 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -26,6 +26,11 @@ Deprecated names
   scanr  : (A → B → B) → B → List A → List B
   ```
 
+* In `Data.List.Properties`:
+  ```agda
+  scanr-defn : scanr f e ≗ map (foldr f e) ∘ tails
+  ```
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
@@ -48,6 +53,11 @@ Additions to existing modules
   scanr  : (A → B → B) → B → List A → List B
   ```
 
+* In `Data.List.NonEmpty.Properties`:
+  ```agda
+  scanr-defn : scanr f e ≗ List.map (List.foldr f e) ∘ List.tails
+  ```
+
 * In `Data.List.Relation.Unary.All.Properties`:
   ```agda
   All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs)
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index 63379cfa56..5fa7d33edc 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -122,7 +122,7 @@ foldl₁ : (A → A → A) → List⁺ A → A
 foldl₁ f = foldl f id
 
 scanr⁺ : (A → B → B) → B → List A → List⁺ B
-scanr⁺ {A = A} {B = B} f e xs = go xs where
+scanr⁺ {A = A} {B = B} f e = go where
   go : List A → List⁺ B
   go []       = e ∷ []
   go (x ∷ xs) = let y ∷ ys = go xs in f x y ∷ y ∷ ys
diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda
index 45b27f46c3..fe866d7f9c 100644
--- a/src/Data/List/NonEmpty/Properties.agda
+++ b/src/Data/List/NonEmpty/Properties.agda
@@ -113,6 +113,16 @@ map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs)
 map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
 map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs)
 
+------------------------------------------------------------------------
+-- scanr
+
+scanr-defn : ∀ (f : A → B → B) (e : B) →
+             scanr f e ≗ List.map (List.foldr f e) ∘ List.tails
+scanr-defn f e []                 = refl
+scanr-defn f e (x ∷ [])           = refl
+scanr-defn f e (x ∷ y∷xs@(_ ∷ _)) = let eq = scanr-defn f e y∷xs in
+  cong₂ (λ z → f x z ∷_) (List.∷-injectiveˡ eq) eq
+
 ------------------------------------------------------------------------
 -- groupSeqs
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 5bd47dc763..4edcd04b4b 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -8,6 +8,7 @@
 -- equalities than _≡_.
 
 {-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated `scanr` (PR #2258)
 
 module Data.List.Properties where
 
@@ -618,18 +619,6 @@ sum-++ (x ∷ xs) ys = begin
 ∈⇒∣product {n} {n ∷ ns} (here  refl) = divides (product ns) (*-comm n (product ns))
 ∈⇒∣product {n} {m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
 
-------------------------------------------------------------------------
--- scanr
-
-scanr-defn : ∀ (f : A → B → B) (e : B) →
-             scanr f e ≗ map (foldr f e) ∘ tails
-scanr-defn f e []             = refl
-scanr-defn f e (x ∷ [])       = refl
-scanr-defn f e (x ∷ y∷xs@(_ ∷ _))
-  with eq ← scanr-defn f e y∷xs
-  with z ∷ zs ← scanr f e y∷xs
-  = let z≡fy⦇f⦈xs , _ = ∷-injective eq in cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq
-
 ------------------------------------------------------------------------
 -- scanl
 
@@ -1292,3 +1281,19 @@ map-─ = map-removeAt
 "Warning: map-─ was deprecated in v2.0.
 Please use map-removeAt instead."
 #-}
+
+-- Version 2.1
+
+scanr-defn : ∀ (f : A → B → B) (e : B) →
+             scanr f e ≗ map (foldr f e) ∘ tails
+scanr-defn f e []             = refl
+scanr-defn f e (x ∷ [])       = refl
+scanr-defn f e (x ∷ y∷xs@(_ ∷ _))
+  with eq ← scanr-defn f e y∷xs
+  with z ∷ zs ← scanr f e y∷xs
+  = let z≡fy⦇f⦈xs , _ = ∷-injective eq in cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq
+{-# WARNING_ON_USAGE scanr-defn
+"Warning: scanr-defn was deprecated in v2.1.
+Please use List.NonEmpty.Properties.scanr-defn instead."
+#-}
+

From d2ebaa1cfcdd7977b69ee2dd7c79cb4be0a2261a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 16 Jan 2024 15:30:05 +0000
Subject: [PATCH 04/14] moved things around, following @gallais's suggestion

---
 CHANGELOG.md                     |  6 +++---
 src/Data/List.agda               | 27 ++++++++++++++++++++++++++-
 src/Data/List/Base.agda          |  2 +-
 src/Data/List/NonEmpty/Base.agda |  5 ++---
 4 files changed, 32 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 46ea38d263..f94ff7e3f7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -50,12 +50,12 @@ Additions to existing modules
 * In `Data.List.NonEmpty.Base`:
   ```agda
   scanr⁺ : (A → B → B) → B → List A → List⁺ B
-  scanr  : (A → B → B) → B → List A → List B
   ```
 
-* In `Data.List.NonEmpty.Properties`:
+* In `Data.List`:
   ```agda
-  scanr-defn : scanr f e ≗ List.map (List.foldr f e) ∘ List.tails
+  scanr      : (A → B → B) → B → List A → List B
+  scanr-defn : scanr f e ≗ map (foldr f e) ∘ tails
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
diff --git a/src/Data/List.agda b/src/Data/List.agda
index 7747cbbd74..0672ddaa6f 100644
--- a/src/Data/List.agda
+++ b/src/Data/List.agda
@@ -11,7 +11,32 @@
 
 module Data.List where
 
+import Data.List.NonEmpty as List⁺
+import Data.List.Properties as List
+open import Function.Base using (_∘_)
+open import Relation.Binary.PropositionalEquality using (refl; cong₂; _≗_)
+
 ------------------------------------------------------------------------
 -- Types and basic operations
 
-open import Data.List.Base public
+open import Data.List.Base public hiding (scanr)
+
+------------------------------------------------------------------------
+-- scanr
+
+module _ {a b} {A : Set a} {B : Set b} where
+
+-- definition
+
+  scanr  : (A → B → B) → B → List A → List B
+  scanr f e = List⁺.toList ∘ List⁺.scanr⁺ f e
+
+-- property
+
+  scanr-defn : ∀ (f : A → B → B) (e : B) →
+               scanr f e ≗ map (foldr f e) ∘ tails
+  scanr-defn f e []                 = refl
+  scanr-defn f e (x ∷ [])           = refl
+  scanr-defn f e (x ∷ y∷xs@(_ ∷ _)) = let eq = scanr-defn f e y∷xs in
+    cong₂ (λ z → f x z ∷_) (List.∷-injectiveˡ eq) eq
+
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 4590d81b3b..a66d46b535 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -574,6 +574,6 @@ scanr f e (x ∷ xs) with scanr f e xs
 ... | y ∷ ys = f x y ∷ y ∷ ys
 {-# WARNING_ON_USAGE scanr
 "Warning: scanr was deprecated in v2.1.
-Please use List.NonEmpty.Base.scanr instead."
+Please use List.scanr instead."
 #-}
 
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index 5fa7d33edc..d022d53adb 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -121,15 +121,14 @@ foldl c s (x ∷ xs) = List.foldl c (s x) xs
 foldl₁ : (A → A → A) → List⁺ A → A
 foldl₁ f = foldl f id
 
+-- Scanr (see `Data.List`).
+
 scanr⁺ : (A → B → B) → B → List A → List⁺ B
 scanr⁺ {A = A} {B = B} f e = go where
   go : List A → List⁺ B
   go []       = e ∷ []
   go (x ∷ xs) = let y ∷ ys = go xs in f x y ∷ y ∷ ys
 
-scanr  : (A → B → B) → B → List A → List B
-scanr f e xs = toList (scanr⁺ f e xs)
-
 -- Append (several variants).
 
 infixr 5 _⁺++⁺_ _++⁺_ _⁺++_

From 61eddec7f5ef476eec32da4cd6be9b0bd8566fc9 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 16 Jan 2024 15:39:20 +0000
Subject: [PATCH 05/14] fixed knock-on errors

---
 src/Data/List/Base.agda                |  4 ++--
 src/Data/List/NonEmpty/Properties.agda | 10 ----------
 src/Data/List/Properties.agda          |  2 +-
 3 files changed, 3 insertions(+), 13 deletions(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index a66d46b535..fd1ee7b55f 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -570,8 +570,8 @@ Please use removeAt instead."
 scanr : (A → B → B) → B → List A → List B
 scanr f e []       = e ∷ []
 scanr f e (x ∷ xs) with scanr f e xs
-... | []     = []                -- dead branch
-... | y ∷ ys = f x y ∷ y ∷ ys
+... | []         = []                -- dead branch
+... | ys@(y ∷ _) = f x y ∷ ys
 {-# WARNING_ON_USAGE scanr
 "Warning: scanr was deprecated in v2.1.
 Please use List.scanr instead."
diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda
index fe866d7f9c..45b27f46c3 100644
--- a/src/Data/List/NonEmpty/Properties.agda
+++ b/src/Data/List/NonEmpty/Properties.agda
@@ -113,16 +113,6 @@ map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs)
 map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
 map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs)
 
-------------------------------------------------------------------------
--- scanr
-
-scanr-defn : ∀ (f : A → B → B) (e : B) →
-             scanr f e ≗ List.map (List.foldr f e) ∘ List.tails
-scanr-defn f e []                 = refl
-scanr-defn f e (x ∷ [])           = refl
-scanr-defn f e (x ∷ y∷xs@(_ ∷ _)) = let eq = scanr-defn f e y∷xs in
-  cong₂ (λ z → f x z ∷_) (List.∷-injectiveˡ eq) eq
-
 ------------------------------------------------------------------------
 -- groupSeqs
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 4edcd04b4b..810dcdba67 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -1294,6 +1294,6 @@ scanr-defn f e (x ∷ y∷xs@(_ ∷ _))
   = let z≡fy⦇f⦈xs , _ = ∷-injective eq in cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq
 {-# WARNING_ON_USAGE scanr-defn
 "Warning: scanr-defn was deprecated in v2.1.
-Please use List.NonEmpty.Properties.scanr-defn instead."
+Please use List.scanr-defn instead."
 #-}
 

From 7a2cb57fd808cf80f2b20dd3810b597f9b13072e Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 16 Jan 2024 16:08:45 +0000
Subject: [PATCH 06/14] =?UTF-8?q?removed=20`scanr=E2=81=BA`=20completely?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                     |  5 -----
 src/Data/List.agda               | 10 ++++++++--
 src/Data/List/NonEmpty/Base.agda |  8 --------
 3 files changed, 8 insertions(+), 15 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f94ff7e3f7..13d2c5cf5b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -47,11 +47,6 @@ Additions to existing modules
   nonZeroIndex : Fin n → ℕ.NonZero n
   ```
 
-* In `Data.List.NonEmpty.Base`:
-  ```agda
-  scanr⁺ : (A → B → B) → B → List A → List⁺ B
-  ```
-
 * In `Data.List`:
   ```agda
   scanr      : (A → B → B) → B → List A → List B
diff --git a/src/Data/List.agda b/src/Data/List.agda
index 0672ddaa6f..b370e34ff0 100644
--- a/src/Data/List.agda
+++ b/src/Data/List.agda
@@ -11,7 +11,7 @@
 
 module Data.List where
 
-import Data.List.NonEmpty as List⁺
+import Data.List.NonEmpty.Base as List⁺
 import Data.List.Properties as List
 open import Function.Base using (_∘_)
 open import Relation.Binary.PropositionalEquality using (refl; cong₂; _≗_)
@@ -26,10 +26,16 @@ open import Data.List.Base public hiding (scanr)
 
 module _ {a b} {A : Set a} {B : Set b} where
 
+  open List⁺ using (List⁺; _∷_; toList)
+
 -- definition
 
   scanr  : (A → B → B) → B → List A → List B
-  scanr f e = List⁺.toList ∘ List⁺.scanr⁺ f e
+  scanr f e = toList ∘ go where
+    go : List A → List⁺ B
+    go []       = e ∷ []
+    go (x ∷ xs) = let y ∷ ys = go xs in f x y ∷ y ∷ ys
+
 
 -- property
 
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index d022d53adb..82f16c270a 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -121,14 +121,6 @@ foldl c s (x ∷ xs) = List.foldl c (s x) xs
 foldl₁ : (A → A → A) → List⁺ A → A
 foldl₁ f = foldl f id
 
--- Scanr (see `Data.List`).
-
-scanr⁺ : (A → B → B) → B → List A → List⁺ B
-scanr⁺ {A = A} {B = B} f e = go where
-  go : List A → List⁺ B
-  go []       = e ∷ []
-  go (x ∷ xs) = let y ∷ ys = go xs in f x y ∷ y ∷ ys
-
 -- Append (several variants).
 
 infixr 5 _⁺++⁺_ _++⁺_ _⁺++_

From 5e68d9e7d96050829afbd5d4c8df95e3b5867207 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Tue, 16 Jan 2024 16:14:25 +0000
Subject: [PATCH 07/14] final cosmetic tweaks

---
 src/Data/List.agda | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Data/List.agda b/src/Data/List.agda
index b370e34ff0..4931361c8e 100644
--- a/src/Data/List.agda
+++ b/src/Data/List.agda
@@ -36,13 +36,11 @@ module _ {a b} {A : Set a} {B : Set b} where
     go []       = e ∷ []
     go (x ∷ xs) = let y ∷ ys = go xs in f x y ∷ y ∷ ys
 
-
 -- property
 
   scanr-defn : ∀ (f : A → B → B) (e : B) →
                scanr f e ≗ map (foldr f e) ∘ tails
   scanr-defn f e []                 = refl
   scanr-defn f e (x ∷ [])           = refl
-  scanr-defn f e (x ∷ y∷xs@(_ ∷ _)) = let eq = scanr-defn f e y∷xs in
+  scanr-defn f e (x ∷ y∷ys@(_ ∷ _)) = let eq = scanr-defn f e y∷ys in
     cong₂ (λ z → f x z ∷_) (List.∷-injectiveˡ eq) eq
-

From 45033830b6e057fd8a37e1c8ca135db2dcfaab3d Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Wed, 17 Jan 2024 10:36:02 +0000
Subject: [PATCH 08/14] `module` parameters

---
 src/Data/List.agda | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/Data/List.agda b/src/Data/List.agda
index 4931361c8e..d1e123d1c3 100644
--- a/src/Data/List.agda
+++ b/src/Data/List.agda
@@ -24,23 +24,22 @@ open import Data.List.Base public hiding (scanr)
 ------------------------------------------------------------------------
 -- scanr
 
-module _ {a b} {A : Set a} {B : Set b} where
+module _ {a b} {A : Set a} {B : Set b} (f : A → B → B) (e : B) where
 
   open List⁺ using (List⁺; _∷_; toList)
 
 -- definition
 
-  scanr  : (A → B → B) → B → List A → List B
-  scanr f e = toList ∘ go where
+  scanr : List A → List B
+  scanr = toList ∘ go where
     go : List A → List⁺ B
     go []       = e ∷ []
     go (x ∷ xs) = let y ∷ ys = go xs in f x y ∷ y ∷ ys
 
 -- property
 
-  scanr-defn : ∀ (f : A → B → B) (e : B) →
-               scanr f e ≗ map (foldr f e) ∘ tails
-  scanr-defn f e []                 = refl
-  scanr-defn f e (x ∷ [])           = refl
-  scanr-defn f e (x ∷ y∷ys@(_ ∷ _)) = let eq = scanr-defn f e y∷ys in
+  scanr-defn : scanr ≗ map (foldr f e) ∘ tails
+  scanr-defn []                 = refl
+  scanr-defn (x ∷ [])           = refl
+  scanr-defn (x ∷ y∷ys@(_ ∷ _)) = let eq = scanr-defn y∷ys in
     cong₂ (λ z → f x z ∷_) (List.∷-injectiveˡ eq) eq

From 239c34b58f5f45ff0684093ad3bc43994242cd3a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 19 Jan 2024 10:32:17 +0000
Subject: [PATCH 09/14] tidied up deprecated proof

---
 src/Data/List/Properties.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 810dcdba67..5fab7af701 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -1288,10 +1288,10 @@ scanr-defn : ∀ (f : A → B → B) (e : B) →
              scanr f e ≗ map (foldr f e) ∘ tails
 scanr-defn f e []             = refl
 scanr-defn f e (x ∷ [])       = refl
-scanr-defn f e (x ∷ y∷xs@(_ ∷ _))
-  with eq ← scanr-defn f e y∷xs
-  with z ∷ zs ← scanr f e y∷xs
-  = let z≡fy⦇f⦈xs , _ = ∷-injective eq in cong₂ (λ z → f x z ∷_) z≡fy⦇f⦈xs eq
+scanr-defn f e (x ∷ xs@(_ ∷ _))
+  with eq ← scanr-defn f e xs
+  with ys@(_ ∷ _) ← scanr f e xs
+  = cong₂ (λ z → f x z ∷_) (∷-injectiveˡ eq) eq
 {-# WARNING_ON_USAGE scanr-defn
 "Warning: scanr-defn was deprecated in v2.1.
 Please use List.scanr-defn instead."

From d0e41a7fd0ce8e9983e2efe8a165c4ce9c4522c7 Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 26 Jan 2024 09:47:17 +0000
Subject: [PATCH 10/14] =?UTF-8?q?redefined=20`scanr`=20in=20terms=20of=20`?=
 =?UTF-8?q?scanr=E2=81=BA`=20etc.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                           | 14 ++++++++++++-
 src/Data/List.agda                     | 19 +++++++-----------
 src/Data/List/NonEmpty/Base.agda       | 15 ++++++++++++++
 src/Data/List/NonEmpty/Properties.agda | 27 ++++++++++++++++++++++++++
 src/Data/List/Properties.agda          |  2 +-
 5 files changed, 63 insertions(+), 14 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 13d2c5cf5b..b4ce40861a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -50,7 +50,19 @@ Additions to existing modules
 * In `Data.List`:
   ```agda
   scanr      : (A → B → B) → B → List A → List B
-  scanr-defn : scanr f e ≗ map (foldr f e) ∘ tails
+  ```
+
+* In `Data.List.NonEmpty.Base`:
+  ```agda
+  tails⁺     : List A → List⁺ (List A)
+  scanr⁺     : (A → B → B) → B → List A → List⁺ B
+  ```
+
+* In `Data.List.NonEmpty.Properties`:
+  ```agda
+  toList-tails⁺ : toList ∘ tails⁺ ≗ List.tails
+  scanr⁺-defn   : scanr⁺ f e ≗ map (List.foldr f e) ∘ tails⁺
+  toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map (List.foldr f e) ∘ List.tails
   ```
 
 * In `Data.List.Relation.Unary.All.Properties`:
diff --git a/src/Data/List.agda b/src/Data/List.agda
index d1e123d1c3..ef77bd0f64 100644
--- a/src/Data/List.agda
+++ b/src/Data/List.agda
@@ -12,9 +12,7 @@
 module Data.List where
 
 import Data.List.NonEmpty.Base as List⁺
-import Data.List.Properties as List
 open import Function.Base using (_∘_)
-open import Relation.Binary.PropositionalEquality using (refl; cong₂; _≗_)
 
 ------------------------------------------------------------------------
 -- Types and basic operations
@@ -26,20 +24,17 @@ open import Data.List.Base public hiding (scanr)
 
 module _ {a b} {A : Set a} {B : Set b} (f : A → B → B) (e : B) where
 
-  open List⁺ using (List⁺; _∷_; toList)
+  open List⁺ using (toList; scanr⁺)
 
 -- definition
 
   scanr : List A → List B
-  scanr = toList ∘ go where
-    go : List A → List⁺ B
-    go []       = e ∷ []
-    go (x ∷ xs) = let y ∷ ys = go xs in f x y ∷ y ∷ ys
+  scanr = toList ∘ scanr⁺ f e
 
--- property
+{-
+-- which satisfies the following property:
 
   scanr-defn : scanr ≗ map (foldr f e) ∘ tails
-  scanr-defn []                 = refl
-  scanr-defn (x ∷ [])           = refl
-  scanr-defn (x ∷ y∷ys@(_ ∷ _)) = let eq = scanr-defn y∷ys in
-    cong₂ (λ z → f x z ∷_) (List.∷-injectiveˡ eq) eq
+  scanr-defn = Data.List.NonEmpty.Properties.toList-scanr⁺
+-}
+
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index 82f16c270a..0d3f0d9e8f 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -143,6 +143,21 @@ concatMap f = concat ∘′ map f
 ap : List⁺ (A → B) → List⁺ A → List⁺ B
 ap fs as = concatMap (λ f → map f as) fs
 
+-- Tails
+
+tails⁺ : List A → List⁺ (List A)
+tails⁺ xs = xs ∷ go xs
+  where
+  go : List A → List (List A)
+  go []       = []
+  go (x ∷ xs) = xs ∷ go xs
+
+-- Scanr
+
+scanr⁺ : (f : A → B → B) (e : B) → List A → List⁺ B
+scanr⁺ f e []       = e ∷ []
+scanr⁺ f e (x ∷ xs) = let y ∷ ys = scanr⁺ f e xs in f x y ∷ y ∷ ys
+
 -- Reverse
 
 reverse : List⁺ A → List⁺ A
diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda
index 45b27f46c3..bf282f0c33 100644
--- a/src/Data/List/NonEmpty/Properties.agda
+++ b/src/Data/List/NonEmpty/Properties.agda
@@ -46,6 +46,9 @@ private
 η : ∀ (xs : List⁺ A) → head xs ∷ tail xs ≡ toList xs
 η _ = refl
 
+toList-injective : {xs ys : List⁺ A} → toList xs ≡ toList ys → xs ≡ ys
+toList-injective refl = refl
+
 toList-fromList : ∀ x (xs : List A) → x ∷ xs ≡ toList (x ∷ xs)
 toList-fromList _ _ = refl
 
@@ -113,6 +116,30 @@ map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs)
 map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
 map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs)
 
+------------------------------------------------------------------------
+-- tails
+
+toList-tails⁺ : toList ∘ tails⁺ ≗ List.tails {A = A}
+toList-tails⁺ []          = refl
+toList-tails⁺ ys@(_ ∷ xs) = cong (ys ∷_) (toList-tails⁺ xs)
+
+------------------------------------------------------------------------
+-- scanr
+
+module _ (f : A → B → B) (e : B) where
+
+  scanr⁺-defn : scanr⁺ f e ≗ map (List.foldr f e) ∘ tails⁺
+  scanr⁺-defn []                = refl
+  scanr⁺-defn (x ∷ [])          = refl
+  scanr⁺-defn (x ∷ xs@(_ ∷ _)) = let eq = scanr⁺-defn xs
+    in cong₂ (λ z → f x z ∷_) (cong head eq) (cong toList eq)
+
+  toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map (List.foldr f e) ∘ List.tails
+  toList-scanr⁺ []                = refl
+  toList-scanr⁺ (x ∷ [])          = refl
+  toList-scanr⁺ (x ∷ xs@(_ ∷ _)) = let eq = toList-scanr⁺ xs
+    in cong₂ (λ z → f x z ∷_) (List.∷-injectiveˡ eq) eq
+
 ------------------------------------------------------------------------
 -- groupSeqs
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 5fab7af701..1f6880a5cf 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -1294,6 +1294,6 @@ scanr-defn f e (x ∷ xs@(_ ∷ _))
   = cong₂ (λ z → f x z ∷_) (∷-injectiveˡ eq) eq
 {-# WARNING_ON_USAGE scanr-defn
 "Warning: scanr-defn was deprecated in v2.1.
-Please use List.scanr-defn instead."
+Please use Data.List.NonEmpty.toList-scanr⁺ instead."
 #-}
 

From 5d1963eedcb6961f07430c72591912b38906008a Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Fri, 26 Jan 2024 09:52:25 +0000
Subject: [PATCH 11/14] missing `CHANGELOG` entry

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b4ce40861a..b9519ca980 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -60,6 +60,8 @@ Additions to existing modules
 
 * In `Data.List.NonEmpty.Properties`:
   ```agda
+  toList-injective : toList xs ≡ toList ys → xs ≡ ys
+  
   toList-tails⁺ : toList ∘ tails⁺ ≗ List.tails
   scanr⁺-defn   : scanr⁺ f e ≗ map (List.foldr f e) ∘ tails⁺
   toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map (List.foldr f e) ∘ List.tails

From 827f530b7b10dbabc413feb79b2ab37bdccf2c5f Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 29 Jan 2024 06:21:38 +0000
Subject: [PATCH 12/14] fix `CHANGELOG`

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b9519ca980..d7fb846196 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -61,7 +61,7 @@ Additions to existing modules
 * In `Data.List.NonEmpty.Properties`:
   ```agda
   toList-injective : toList xs ≡ toList ys → xs ≡ ys
-  
+
   toList-tails⁺ : toList ∘ tails⁺ ≗ List.tails
   scanr⁺-defn   : scanr⁺ f e ≗ map (List.foldr f e) ∘ tails⁺
   toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map (List.foldr f e) ∘ List.tails

From f782b3e31b0d616d15c34a0a016881475d4935bd Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 29 Jan 2024 08:44:27 +0000
Subject: [PATCH 13/14] simplified and refactored proofs

---
 CHANGELOG.md                           |  2 +-
 src/Data/List/NonEmpty/Properties.agda | 20 +++++++++++++-------
 2 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d7fb846196..18403ba3a5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -61,7 +61,7 @@ Additions to existing modules
 * In `Data.List.NonEmpty.Properties`:
   ```agda
   toList-injective : toList xs ≡ toList ys → xs ≡ ys
-
+  toList-map    : (f : A → B) → toList ∘ map f ≗ List.map f ∘ toList
   toList-tails⁺ : toList ∘ tails⁺ ≗ List.tails
   scanr⁺-defn   : scanr⁺ f e ≗ map (List.foldr f e) ∘ tails⁺
   toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map (List.foldr f e) ∘ List.tails
diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda
index bf282f0c33..be73d38e9f 100644
--- a/src/Data/List/NonEmpty/Properties.agda
+++ b/src/Data/List/NonEmpty/Properties.agda
@@ -116,6 +116,9 @@ map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (List.map-cong f≗g xs)
 map-∘ : {g : B → C} {f : A → B} → map (g ∘ f) ≗ map g ∘ map f
 map-∘ (x ∷ xs) = cong (_ ∷_) (List.map-∘ xs)
 
+toList-map : (f : A → B) → toList ∘ map f ≗ List.map f ∘ toList
+toList-map f (x ∷ xs) = refl
+
 ------------------------------------------------------------------------
 -- tails
 
@@ -129,16 +132,19 @@ toList-tails⁺ ys@(_ ∷ xs) = cong (ys ∷_) (toList-tails⁺ xs)
 module _ (f : A → B → B) (e : B) where
 
   scanr⁺-defn : scanr⁺ f e ≗ map (List.foldr f e) ∘ tails⁺
-  scanr⁺-defn []                = refl
-  scanr⁺-defn (x ∷ [])          = refl
-  scanr⁺-defn (x ∷ xs@(_ ∷ _)) = let eq = scanr⁺-defn xs
+  scanr⁺-defn []       = refl
+  scanr⁺-defn (x ∷ xs) = let eq = scanr⁺-defn xs
     in cong₂ (λ z → f x z ∷_) (cong head eq) (cong toList eq)
 
   toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map (List.foldr f e) ∘ List.tails
-  toList-scanr⁺ []                = refl
-  toList-scanr⁺ (x ∷ [])          = refl
-  toList-scanr⁺ (x ∷ xs@(_ ∷ _)) = let eq = toList-scanr⁺ xs
-    in cong₂ (λ z → f x z ∷_) (List.∷-injectiveˡ eq) eq
+  toList-scanr⁺ xs = begin
+    toList (scanr⁺ f e xs)
+      ≡⟨ cong toList (scanr⁺-defn xs) ⟩
+    toList (map (List.foldr f e) (tails⁺ xs))
+      ≡⟨ toList-map _ (tails⁺ xs) ⟩
+    List.map (List.foldr f e) (toList (tails⁺ xs))
+      ≡⟨ cong (List.map (List.foldr f e)) (toList-tails⁺ xs) ⟩
+    List.map (List.foldr f e) (List.tails xs) ∎
 
 ------------------------------------------------------------------------
 -- groupSeqs

From e16bf5551c3406467b8aefa445dd7fb2057af1cf Mon Sep 17 00:00:00 2001
From: James McKinna <J.McKinna@hw.ac.uk>
Date: Mon, 29 Jan 2024 08:57:12 +0000
Subject: [PATCH 14/14] local definition, for readability

---
 src/Data/List/NonEmpty/Properties.agda | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda
index be73d38e9f..7590341b8e 100644
--- a/src/Data/List/NonEmpty/Properties.agda
+++ b/src/Data/List/NonEmpty/Properties.agda
@@ -131,20 +131,23 @@ toList-tails⁺ ys@(_ ∷ xs) = cong (ys ∷_) (toList-tails⁺ xs)
 
 module _ (f : A → B → B) (e : B) where
 
-  scanr⁺-defn : scanr⁺ f e ≗ map (List.foldr f e) ∘ tails⁺
+  private
+    h = List.foldr f e
+
+  scanr⁺-defn : scanr⁺ f e ≗ map h ∘ tails⁺
   scanr⁺-defn []       = refl
   scanr⁺-defn (x ∷ xs) = let eq = scanr⁺-defn xs
     in cong₂ (λ z → f x z ∷_) (cong head eq) (cong toList eq)
 
-  toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map (List.foldr f e) ∘ List.tails
+  toList-scanr⁺ : toList ∘ scanr⁺ f e ≗ List.map h ∘ List.tails
   toList-scanr⁺ xs = begin
     toList (scanr⁺ f e xs)
       ≡⟨ cong toList (scanr⁺-defn xs) ⟩
-    toList (map (List.foldr f e) (tails⁺ xs))
-      ≡⟨ toList-map _ (tails⁺ xs) ⟩
-    List.map (List.foldr f e) (toList (tails⁺ xs))
-      ≡⟨ cong (List.map (List.foldr f e)) (toList-tails⁺ xs) ⟩
-    List.map (List.foldr f e) (List.tails xs) ∎
+    toList (map h (tails⁺ xs))
+      ≡⟨ toList-map h (tails⁺ xs) ⟩
+    List.map h (toList (tails⁺ xs))
+      ≡⟨ cong (List.map h) (toList-tails⁺ xs) ⟩
+    List.map h (List.tails xs) ∎
 
 ------------------------------------------------------------------------
 -- groupSeqs