Function extern_spec_T_MaybeUninit_T_assume_init_mut 

pub unsafe fn extern_spec_T_MaybeUninit_T_assume_init_mut<T>(
    self_: &mut MaybeUninit<T>,
) -> &mut T

extern spec for MaybeUninit<T>::assume_init_mut

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

requires

self@ != None

ensures

(*self)@ == Some(*result) && (^self)@ == Some(^result)

terminates

ghost