Compare commits

...

1 Commits

Author SHA1 Message Date
Kim Morrison
7624298c68 chore: List.filterMapM runs and returns left-to-right 2024-07-24 18:43:58 +10:00
2 changed files with 5 additions and 5 deletions

View File

@@ -127,12 +127,12 @@ results `y` for which `f x` returns `some y`.
@[inline]
def filterMapM {m : Type u Type v} [Monad m] {α β : Type u} (f : α m (Option β)) (as : List α) : m (List β) :=
let rec @[specialize] loop
| [], bs => pure bs
| [], bs => pure bs.reverse
| a :: as, bs => do
match ( f a) with
| none => loop as bs
| some b => loop as (b::bs)
loop as.reverse []
loop as []
/--
Folds a monadic function over a list from left to right:

View File

@@ -58,10 +58,10 @@ def tst : IO (List Nat) :=
(if x % 2 == 0 then pure $ some (x + 10) else pure none)
/--
info: 4
3
info: 1
2
1
3
4
[12, 14]
-/
#guard_msgs in