leading_bits_width_1

Function leading_bits_width_1 

Source
pub open spec fn leading_bits_width_1(byte: u8) -> u32
Expand description
recommends
is_leading_byte_width_1(byte),
{ (byte & 0x7F) as u32 }

Value of the 7 data bits from the given byte, assuming that it is a valid leading byte for a 1-byte UTF-8 encoding.