Function extern_spec_T_MaybeUninit_T_write 

pub fn extern_spec_T_MaybeUninit_T_write<T>(
    self_: &mut MaybeUninit<T>,
    val: T,
) -> &mut T

extern spec for MaybeUninit<T>::write

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

requires

self@ == None

ensures

*result == val

ensures

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

terminates

ghost