From f694e5e2f0ceb38e9487fc59157f2e545c08eed4 Mon Sep 17 00:00:00 2001
From: Raffi Sanna <rvs314@protonmail.com>
Date: Wed, 18 Oct 2023 18:39:15 -0400
Subject: [PATCH] Use `do` notation in `some`

---
 libs/contrib/Data/String/Parser.idr | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/libs/contrib/Data/String/Parser.idr b/libs/contrib/Data/String/Parser.idr
index fb536432df..4de6f12f4c 100644
--- a/libs/contrib/Data/String/Parser.idr
+++ b/libs/contrib/Data/String/Parser.idr
@@ -208,7 +208,9 @@ mutual
     export
     covering
     some : Monad m => ParseT m a -> ParseT m (List a)
-    some p = [| p :: many p |]
+    some p = do r <- p
+                rs <- many p
+                pure $ r :: rs
 
     ||| Always succeeds, will accumulate the results of `p` in a list until it fails.
     export