Skip to main content

copy_within_result

vstd::std_specs::slice

Function copy_within_result 

Source 
pub open spec fn copy_within_result<T>(
    old_slice: Seq<T>,
    src_start: int,
    src_end: int,
    dest: int,
) -> Seq<T>
Expand description
{
    let count = src_end - src_start;
    Seq::new(
        old_slice.len(),
        |i: int| {
            if dest <= i && i < dest + count {
                old_slice[src_start + (i - dest)]
            } else {
                old_slice[i]
            }
        },
    )
}

The sequence resulting from copying old_slice[src_start..src_end] to start at index dest, leaving all other positions unchanged. Reads are taken from old_slice, so overlapping source and destination ranges are handled like std’s <[T]>::copy_within (which uses ptr::copy).