leading_byte_width_1

Function leading_byte_width_1 

Source
pub open spec fn leading_byte_width_1(scalar: u32) -> u8
Expand description
recommends
has_width_1_encoding(scalar),
{ (scalar & 0x7F) as u8 }

The first (and only) byte of the UTF-8 encoding of the given scalar value, assuming that the scalar has a 1-byte UTF-8 encoding.