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):
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
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