Zulip Chat Archive

Stream: general

Topic: string munging

Scott Morrison (Mar 22 2019 at 00:29):

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 (Mar 22 2019 at 00:29):

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

Simon Hudon (Mar 22 2019 at 03:40):

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

Keeley Hoek (Mar 23 2019 at 01:19):

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

Last updated: Dec 20 2023 at 11:08 UTC