pop_first_scalar

Function pop_first_scalar 

Source
pub open spec fn pop_first_scalar(bytes: Seq<u8>) -> Seq<u8>
Expand description
recommends
valid_first_scalar(bytes),
{ bytes.subrange(length_of_first_scalar(bytes), bytes.len() as int) }

Removes the first scalar encoded in UTF-8 in the given byte sequence and returns the rest of the sequence, assuming that the sequence begins with a well-formed encoding of a single scalar.