Zulip Chat Archive

Stream: Is there code for X?

Topic: interweaved list


view this post on Zulip 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

view this post on Zulip Adam Topaz (Sep 23 2020 at 15:53):

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

view this post on Zulip Adam Topaz (Sep 23 2020 at 15:55):

Oh nevermind... You want a type

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 23 2020 at 16:53):

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

view this post on Zulip Eric Wieser (Sep 23 2020 at 17:27):

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

view this post on Zulip 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.

view this post on Zulip 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