decode_utf8

Function decode_utf8 

Source
pub open spec fn decode_utf8(bytes: Seq<u8>) -> Seq<char>
Expand description
recommends
valid_utf8(bytes),
{
    if bytes.len() == 0 {
        seq![]
    } else {
        seq![decode_first_scalar(bytes) as char] + decode_utf8(pop_first_scalar(bytes))
    }
}

The sequence of characters encoded as Unicode scalars in the given bytes, assuming that the bytes form a valid UTF-8 encoding.