Stream: Beginner Questions

Topic: splitWith missing in List.thy ?


view this post on Zulip Robert Soeldner (Jul 05 2021 at 19:50):

I was looking for splitWith, like
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?

view this post on Zulip Manuel Eberl (Jul 05 2021 at 19:53):

You're looking for partition.

view this post on Zulip Robert Soeldner (Jul 05 2021 at 19:54):

ha :-) thank you

view this post on Zulip Manuel Eberl (Jul 05 2021 at 19:56):

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.

view this post on Zulip Manuel Eberl (Jul 05 2021 at 19:56):

(The definition/code equations are basically equivalent to your fold.)

view this post on Zulip Robert Soeldner (Jul 05 2021 at 19:57):

good to know, thank you


Last updated: Sep 25 2021 at 08:21 UTC