Interpret ByteArray as a String

Stream: lean4

[cognivore]

Does anyone knows how to tell Lean "extract all the Utf-8-encoded Unicode into a String from a ByteArray"? I know I could, in principle, roll my own with a fold, but I really don't want to :D

[Sebastian Ullrich]

docs4#String.fromUTF8Unchecked