list.split_sum

Stream: Is there code for X?

[Johan Commelin]

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))

[Simon Hudon]

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

[Kenny Lau]

this is an equiv right

[Simon Hudon]

no

[Simon Hudon]

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

[Kyle Miller]

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

[Johan Commelin]

Nice, thanks!