valid_leading_and_continuation_bytes_first_codepoint

vstd::utf8

Function valid_leading_and_continuation_bytes_first_codepoint 

Source 
pub open spec fn valid_leading_and_continuation_bytes_first_codepoint(
    bytes: Seq<u8>,
) -> bool
Expand description
{
    ||| (bytes.len() >= 1 && is_leading_byte_width_1(bytes[0]))
    ||| (bytes.len() >= 2 && is_leading_byte_width_2(bytes[0])
        && is_continuation_byte(bytes[1]))
    ||| (bytes.len() >= 3 && is_leading_byte_width_3(bytes[0])
        && is_continuation_byte(bytes[1]) && is_continuation_byte(bytes[2]))
    ||| (bytes.len() >= 4 && is_leading_byte_width_4(bytes[0])
        && is_continuation_byte(bytes[1]) && is_continuation_byte(bytes[2])
        && is_continuation_byte(bytes[3]))

}

True when the given byte sequence begins with a well-formed leading byte and an appropriate number of well-formed continuation bytes for a UTF-8 encoding of a single codepoint.