Stream: Is there code for X?

Topic: interweaved list

Eric Wieser (Sep 23 2020 at 15:41):

Does a type like the following exist already?

inductive interweaved (α β : Type*)
| part : α → interweaved
| separator : α → β → interweaved → interweaved


This is a list that alternates [α, β, ..., β, α], like what you might get from splitting a string

Adam Topaz (Sep 23 2020 at 15:53):

Haskell has the intersperse function. Presumably lean has something similar?

Adam Topaz (Sep 23 2020 at 15:55):

Oh nevermind... You want a type

Eric Wieser (Sep 23 2020 at 15:59):

Perhaps interspersed is a better name. docs#list.intercalate and docs#list.intersperse are both things, but they only support the case when the β terms have a uniform value

Mario Carneiro (Sep 23 2020 at 16:53):

I guess that's just A x list (B x A)

Eric Wieser (Sep 23 2020 at 17:27):

It's not, because that type doesn't have an equivalent to interweaved.part a

Eric Wieser (Sep 23 2020 at 17:28):

A \oplus (A x list (B x A)) perhaps, but that's probably harder to work with.

Eric Wieser (Sep 23 2020 at 17:29):

Yeah, that probably would work just fine too, good point

Last updated: May 17 2021 at 15:13 UTC