Copy slice of String to end of other String?

Stream: lean4

[Thomas Murrills]

In the new String API, what’s the most performant way to copy the substring between two positions in s1 : String onto the end of some s2 : String? (Here I mean the colloquial “substring”, not necessarily Substring.)

Should I extract (copy) the slice from s1 into its own string, then append to s2? Or should I iterate through positions of s1 from the starting position to the final one and push the new characters onto s2 one-by-one? (Or something else? Have I simply missed the API for this?)

Note: my broader goal here is to apply a bunch of edits (defined by ranges of positions together with the new string that should replace that range) to create s2 from the source s1, so I will still need access to s1 after copying unmodified stretches over to s2. (I am open to completely different approaches to modifying multiple regions in s1, though.)

I could just test, but I’d like to build some understanding of “why” if possible, which might be useful more generally. :)

Thanks! :)

[Markus Himmel]

In recent enough versions of Lean there is a HAppend String String.Slice String instance for this use case. Its implementation is currently not the best it could be, but it will be improved.

[Thomas Murrills]

Great! I'll rely on that, and let the performance improvements come when they come. :grinning_face_with_smiling_eyes: