String.reverse

Stream: general

[Maris Ozols]

Not sure if I'm posting this in the right channel...

The last example in List.map and List.mapTr use String.reverse but the latest version of Lean (lean4:v4.26.0) doesn't seem to have such function. I ended up implementing it myself using List.reverse:

def reverse (s : String) : String :=
  String.ofList s.toList.reverse

[Henrik Böving]

You could potentially use String.revChars instead.

[Alfredo Moreira-Rosa]

revChars and List.reverse seems to break uft8 composed emojis :

#eval String.ofList "1️⃣2️⃣3️⃣4️⃣5️⃣6️⃣7️⃣0️⃣".revChars.toList -- "⃣️0⃣️7⃣️6⃣️5⃣️4⃣️3⃣️2⃣️1"
#eval String.ofList "1️⃣2️⃣3️⃣4️⃣5️⃣6️⃣7️⃣0️⃣".toList.reverse --  "⃣️0⃣️7⃣️6⃣️5⃣️4⃣️3⃣️2⃣️1"

does lean support graphemes splitting ?
Here a working js solution :

function reverseString(str) {
  const segmenter = new Intl.Segmenter(undefined, { granularity: 'grapheme' })
  return [...segmenter.segment(str)]
    .map(s => s.segment)
    .reverse()
    .join('')
}
reverseString("1️⃣2️⃣3️⃣4️⃣5️⃣6️⃣7️⃣0️⃣") // '0️⃣7️⃣6️⃣5️⃣4️⃣3️⃣2️⃣1️⃣'

Is this also possible with Lean API ?

[Weiyi Wang]

This kind of unicode problem is always a nightmare in any programming language. It boils down to one question "what is a character"

[Alfredo Moreira-Rosa]

Maybe it's just an API issue and behind the scene Lean understand unicode graphemes (composition of many code points that represent a single visual element)?

[Henrik Böving]

No, Lean, just like Rust's stdlib, decided to not support graphemes, the unit of character is a unicode scalar value.

[Alfredo Moreira-Rosa]

Thanks for the insight. Seems like a fun small project for a reservoir library :)