is_char_boundary_start_end_of_seq

vstd::utf8

Function is_char_boundary_start_end_of_seq 

Source 
pub broadcast proof fn is_char_boundary_start_end_of_seq(bytes: Seq<u8>)
Expand description
requires
valid_utf8(bytes),
ensures
is_char_boundary(bytes, 0),
is_char_boundary(bytes, bytes.len() as int),

Ensures that the start and end of a valid UTF-8 byte sequence are character boundaries.