pub open spec fn decode_bmp_string(bytes: Seq<u8>) -> Seq<char>
{ Seq::new(bytes.len() / 2, |i: int| bmp_code_unit(bytes, i) as char) }
Decode two-octet big-endian BMP/UCS-2 code units.