length_of_first_codepoint

vstd::utf8

Function length_of_first_codepoint 

Source 
pub open spec fn length_of_first_codepoint(bytes: Seq<u8>) -> int
Expand description
recommends
valid_leading_and_continuation_bytes_first_codepoint(bytes),
{
    if is_leading_byte_width_1(bytes[0]) {
        1
    } else if is_leading_byte_width_2(bytes[0]) {
        2
    } else if is_leading_byte_width_3(bytes[0]) {
        3
    } else {
        4
    }
}

The length in bytes of 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.