interweaved list

Stream: Is there code for X?

[Eric Wieser]

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]

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

[Adam Topaz]

Oh nevermind... You want a type

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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