decode_utf8_first_scalar

Function decode_utf8_first_scalar 

Source
pub proof fn decode_utf8_first_scalar(bytes: Seq<u8>)
Expand description
requires
valid_utf8(bytes),
bytes.len() > 0,
ensures
encode_scalar((decode_first_scalar(bytes) as char) as u32) == take_first_scalar(bytes),

Properties of the first scalar from the result of decode_utf8.