pub open spec fn seq_splice(data: Seq<u8>, pos: usize, v: Seq<u8>) -> Seq<u8>Expand description
recommends
pos + v.len() <= data.len(),{ data.take(pos as int) + v + data.skip(pos + v.len() as int) }Helper function to splice a sequence of bytes into another sequence of bytes.