in the library already?

Stream: general

[Scott Morrison]

Is this in the library somewhere?

def list.split_on_aux {α} [decidable_eq α] (a : α) : list α → list α → list (list α)
| [] l       := [l.reverse]
| (h :: t) l := if h = a then
                  l.reverse :: (list.split_on_aux t [])
                else
                  list.split_on_aux t (h :: l)

def list.split_on {α} [decidable_eq α] (a : α) : list α → list (list α)
| l := list.split_on_aux a l []