is_leading_byte_width_1

Function is_leading_byte_width_1 

Source
pub open spec fn is_leading_byte_width_1(byte: u8) -> bool
Expand description
{ 0x00 <= byte <= 0x7f }

True when the given byte conforms to the bit pattern for the first byte of a 1-byte UTF-8 encoding of a single codepoint. The byte must have the form 0xxxxxxx.