Function extern_spec_T__slice_MaybeUninit_T_assume_init_ref 

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

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

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

ghost

requires

self@.len() ==> self

ensures

self

ensures

self@.len() ==> self