Combining IO and Reader uses String.separate instead of String.intercalate

[bjornestol]

Please quote the text that is incorrect:

IO.eprintln s!"Didn't understand argument(s) {" ".separate args}\n"

In what way is this incorrect?

I don't know if this counts as a technical error or typo, as it pertains to non-working code.
Unless I'm mistaken, String.separate does not exist, and the correct code would be String.intercalate. Only the latter works for me and I cannot find String.separate in the lean4 source code.