From 9148fa597f7a871df856356478c91f7684b489bf Mon Sep 17 00:00:00 2001
From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
Date: Sat, 20 Apr 2024 05:19:23 +0100
Subject: [PATCH] Improve `Data.List.Base.unfold` (#2359; deprecate use of
 `with` #2123) (#2364)

* `with`-free definition of `unfold`

* fixed previous commit
---
 src/Data/List/Base.agda | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 03e5d4ae9a..bc31ca0f9e 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -250,9 +250,7 @@ unfold : ∀ (P : ℕ → Set b)
          (f : ∀ {n} → P (suc n) → Maybe (A × P n)) →
          ∀ {n} → P n → List A
 unfold P f {n = zero}  s = []
-unfold P f {n = suc n} s with f s
-... | nothing       = []
-... | just (x , s′) = x ∷ unfold P f s′
+unfold P f {n = suc n} s = maybe′ (λ (x , s′) → x ∷ unfold P f s′) [] (f s)
 
 ------------------------------------------------------------------------
 -- Operations for reversing lists