Skip to content

Commit

Permalink
chore: List.filterMapM runs and returns left-to-right (#4820)
Browse files Browse the repository at this point in the history
Closes #4676. Previously `List.filterMapM` was returning results
left-to-right, but evaluating right-to-left.
  • Loading branch information
kim-em authored Jul 24, 2024
1 parent 3701bee commit 1758b37
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 5 deletions.
4 changes: 2 additions & 2 deletions src/Init/Data/List/Control.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
6 changes: 3 additions & 3 deletions tests/lean/run/array1.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 1758b37

Please sign in to comment.