Function extern_spec_T_MaybeUninit_T_assume_init_drop 

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

extern spec for MaybeUninit<T>::assume_init_drop

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

requires

self@ != None

ensures

(^self)@ == None

terminates

ghost