I was looking for
fun splitWith :: "'a list ⇒ ('a ⇒ bool) ⇒ 'a list × 'a list" where
"splitWith t p = foldr (λe (l,r). if p e then (e#l,r) else (l, e#r)) t (,)"
any reason it (and friends) are not in the List theory?
You're looking for
ha :-) thank you
If you want to export code, note that the default code equations from the library may not be terribly efficient depending on your target language.
(The definition/code equations are basically equivalent to your fold.)
good to know, thank you
Last updated: Aug 10 2022 at 19:17 UTC