Function extern_spec_T__slice_T_copy_from_slice 

pub fn extern_spec_T__slice_T_copy_from_slice<T>(self_: &mut [T], src: &[T])
where
    T: Copy,

extern spec for slice<T>::copy_from_slice

This is not a real function: its only use is for documentation.

terminates

ghost

requires

self@.len() == src@.len()

ensures

(^self)@ == src@