is_char_boundary

vstd::utf8

Function is_char_boundary 

Source 
pub open spec fn is_char_boundary(bytes: Seq<u8>, index: int) -> bool
Expand description
recommends
valid_utf8(bytes),
{
    if index == 0 {
        true
    } else if index < 0 || bytes.len() < index {
        false
    } else {
        is_char_boundary(pop_first_scalar(bytes), index - length_of_first_scalar(bytes))
    }
}

True when the given index into the byte sequence is the first byte of a character’s encoding or the end of the sequence, assuming that the sequence is valid UTF-8.