length_of_first_scalar

vstd::utf8

Function length_of_first_scalar 

Source 
pub open spec fn length_of_first_scalar(bytes: Seq<u8>) -> int
Expand description
recommends
valid_first_scalar(bytes),
{ length_of_first_codepoint(bytes) }

The length in bytes of first scalar encoded in UTF-8 in the given byte sequence, assuming that the sequence begins with a well-formed encoding of a single scalar.