You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
List.filterMapM works from right to left, not left to right as the documentation claims.
-- for reference. output: 123#eval discard $ [1, 2, 3].mapM fun x => IO.print x
-- expected: 123, actual: 321#eval discard $ [1, 2, 3].filterMapM fun x => some <$> IO.print x
Versions
"4.11.0-nightly-2024-07-07" on live.lean-lang.org
Additional information
I tested these other monadic map-like functions and they all seem to behave as advertised:
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
List.filterMapM
works from right to left, not left to right as the documentation claims.Versions
"4.11.0-nightly-2024-07-07"
onlive.lean-lang.org
Additional information
I tested these other monadic
map
-like functions and they all seem to behave as advertised:List
:mapM
,forM
,filterM
,filterRevM
,foldlM
,foldrM
Array
: the above (exceptArray.filterRevM
which doesn't exist) and, notably,filterMapM
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: