decode_first_codepoint

vstd::utf8

Function decode_first_codepoint 

Source 
pub open spec fn decode_first_codepoint(bytes: Seq<u8>) -> u32
Expand description
recommends
valid_leading_and_continuation_bytes_first_codepoint(bytes),
{
    if is_leading_byte_width_1(bytes[0]) {
        codepoint_width_1(bytes[0])
    } else if is_leading_byte_width_2(bytes[0]) {
        codepoint_width_2(bytes[0], bytes[1])
    } else if is_leading_byte_width_3(bytes[0]) {
        codepoint_width_3(bytes[0], bytes[1], bytes[2])
    } else {
        codepoint_width_4(bytes[0], bytes[1], bytes[2], bytes[3])
    }
}

Returns the first codepoint encoded in UTF-8 in the given byte sequence, assuming that the sequence begins with a well-formed leading byte and an appropriate number of well-formed continuation bytes.