Zulip Chat Archive

Stream: general

Topic: string munging


view this post on Zulip 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?

view this post on Zulip Scott Morrison (Mar 22 2019 at 00:29):

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

view this post on Zulip 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

view this post on Zulip 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: May 13 2021 at 16:25 UTC