Skip to main content

extern_spec_T__slice_MaybeUninit_T_write_copy_of_slice

creusot_std::std::mem

Function extern_spec_T__slice_MaybeUninit_T_write_copy_of_slice 

Source 
pub fn extern_spec_T__slice_MaybeUninit_T_write_copy_of_slice<'a, T>(
    self_: &'a mut [MaybeUninit<T>],
    src: &[T],
) -> &'a mut [T]
where
    T: Copy,
Expand description

extern spec for slice<MaybeUninit<T>>::write_copy_of_slice

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

ghost

requires 

self

ensures 

(*self)@.len() == (*result)@.len()

ensures 

(^self)@.len() == (^result)@.len()

ensures 

(*result)@.len() == (^result)@.len()

ensures 

self

ensures 

self