Zulip Chat Archive

Stream: Is there code for X?

Topic: list.split_sum


view this post on Zulip Johan Commelin (Jul 07 2020 at 14:15):

Am I duplicating things?

def list.split_sum : list (α  β)  (list α) × (list β)
| []  := ([], [])
| ((sum.inl a) :: l) := let L := l.split_sum in ((a :: L.1), L.2)
| ((sum.inr b) :: l) := let L := l.split_sum in (L.1, (b :: L.2))

view this post on Zulip Simon Hudon (Jul 07 2020 at 14:19):

I don't have mathlib open but you can look for partition, partition_map or partition_sum in data.list.defs or in the core definitions

view this post on Zulip Kenny Lau (Jul 07 2020 at 14:20):

this is an equiv right

view this post on Zulip Simon Hudon (Jul 07 2020 at 14:21):

no

view this post on Zulip Simon Hudon (Jul 07 2020 at 14:22):

[sum.inl 3, sum.inr 1] and [sum.inr 1, sum.inl 3] both map to the same input

view this post on Zulip Kyle Miller (Jul 07 2020 at 19:38):

Simon Hudon said:

I don't have mathlib open but you can look for partition, partition_map or partition_sum in data.list.defs or in the core definitions

It looks like partition_map works:

def list.split_sum : list (α  β)  list α × list β
:= list.partition_map id

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:47):

Nice, thanks!


Last updated: May 16 2021 at 05:21 UTC