working with strings

Stream: general

[Jon Eugster]

I need some help with String operations.

a) given a String of unknown length, how do I get a slice of it, like python's s[:7]?
b) how do I join an Array/List of Strings (like python's '-'.join(a))?

[Adam Topaz]

for the second we do have docs#String.intercalate

[Adam Topaz]

I don't know what python's join does, but I assume it's the same?

[Adam Topaz]

For the slice, I think we're meant to use docs#Substring but I don't know whether there is a nice slice notation

[Jon Eugster]

Adam Topaz said:

I don't know what python's join does, but I assume it's the same?

Thanks, intercalate is exactly what I was looking for. For Substring, I figured that the indexes need to be ⟨7⟩ and not a plain 7:

let s₂ : Substring := ⟨s, ⟨0⟩, ⟨7⟩⟩

I wonder if there should be an instance

instance : OfNat String.Pos x where
  ofNat := {
    byteIdx := x
  }

so one could simply write let s₂ : Substring := ⟨s, 0, 7⟩. Or maybe it exists somewhere and I didn't import it.

[Adam Topaz]

I would hope that we can introduce slice notation for substrings similar to how we can use slice notation for subarrays