decode_first_scalar

Function decode_first_scalar 

Source
pub open spec fn decode_first_scalar(bytes: Seq<u8>) -> u32
Expand description
recommends
valid_first_scalar(bytes),
{ decode_first_codepoint(bytes) }

The 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.