extern_spec_std_ops_DerefMut_deref_mut

creusot_contracts::std::ops

Function extern_spec_std_ops_DerefMut_deref_mut 

Source 
pub fn extern_spec_std_ops_DerefMut_deref_mut<Self_>(
    self_: &mut Self_,
) -> &mut Self_::Target
where
    Self_: ?Sized + DerefMut,
Expand description

extern spec for ::std::ops::DerefMut::deref_mut

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

terminates

ghost

requires 

false