string munging

Stream: general

[Scott Morrison]

Is there an API for strings that e.g. lets me drop the first n characters of a string? Lets me remove a given prefix, if it appears?

[Scott Morrison]

So far for the first question my solution was (s.mk_iterator.remove n).to_string.

[Simon Hudon]

I've been using string.to_list and then list operations but I'm not sure that it's efficient

[Keeley Hoek]

In my experience parsing big files of serialised exprs, the iterator api was slower than using lists for char-by-char manipulation. I think native part has optimised versions of the remove n etc. family stuff, though