take_first_scalar

Function take_first_scalar 

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

Takes the bytes corresponding to the first scalar encoded in UTF-8 in the given byte sequence, assuming that the sequence begins with a well-formed encoding of a single scalar.