pub proof fn decode_utf8_first_scalar(bytes: Seq<u8>)Expand description
requires
valid_utf8(bytes),bytes.len() > 0,ensuresencode_scalar((decode_first_scalar(bytes) as char) as u32) == take_first_scalar(bytes),Properties of the first scalar from the result of decode_utf8.