Use do notation in some

idris-lang · Oct 19, 2023 · f694e5e · f694e5e
1 parent 6c35157
commit f694e5e
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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