From 5cae4063924d4d02c67c7e62dde3c2348888e5f2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 15 Apr 2024 16:03:42 +0100
Subject: [PATCH 1/2] `with`-free definition of `unfold`

---
 src/Data/List/Base.agda | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 8b988c646d..8e727e1b15 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -253,10 +253,12 @@ 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
+unfold P f {n = suc n} s = maybe′ {!λ (x , s′) → x ∷ unfold P f s′!} [] (f s)
+{-
+with f s
 ... | nothing       = []
 ... | just (x , s′) = x ∷ unfold P f s′
-
+-}
 ------------------------------------------------------------------------
 -- Operations for reversing lists
 

From 854dfcf93c54cb8018a51297bb3b6fff717a64f9 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 15 Apr 2024 16:37:04 +0100
Subject: [PATCH 2/2] fixed previous commit

---
 src/Data/List/Base.agda | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 8e727e1b15..168c5ca91f 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -253,12 +253,8 @@ 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 = maybe′ {!λ (x , s′) → x ∷ unfold P f s′!} [] (f 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