Zulip Chat Archive
Stream: Is there code for X?
Topic: Finset filter map
Marcus Rossel (Apr 19 2022 at 19:58):
Is there some function like:
def finset.filter_map (f : finset X) (g : X -> option Y) : finset Y
... such that f.filter_map g
contains all values resulting from mapping f
through g
which are not none
?
Yaël Dillies (Apr 19 2022 at 20:00):
def finset.filter_map (f : finset X) (g : X -> option Y) : finset Y :=
(f.map g).erase_none
Last updated: Dec 20 2023 at 11:08 UTC