Function extern_spec_T__slice_MaybeUninit_T_assume_init_mut 

pub unsafe fn extern_spec_T__slice_MaybeUninit_T_assume_init_mut<T>(
    self_: &mut [MaybeUninit<T>],
) -> &mut [T]

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

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