encode_utf8

Function encode_utf8 

Source
pub open spec fn encode_utf8(chars: Seq<char>) -> Seq<u8>
Expand description
{
    if chars.len() == 0 {
        seq![]
    } else {
        encode_scalar(chars[0] as u32) + encode_utf8(chars.drop_first())
    }
}

The UTF-8 encoding of the given char sequence.