pub fn extern_spec_T_Default__refmut__slice_T_default<'a, T>() -> &'a mut [T]Expand description
extern spec for [&mut slice<T>::default]
This is not a real function: its only use is for documentation.
terminates
ghost
ensures
(*result)@ == Seq::empty()ensures
(^result)@ == Seq::empty()