Skip to main content

extern_spec_T__slice_T_split_at_mut

creusot_std::std::slice

Function extern_spec_T__slice_T_split_at_mut 

Source 
pub fn extern_spec_T__slice_T_split_at_mut<T>(
    self_: &mut [T],
    mid: usize,
) -> (&mut [T], &mut [T])
Expand description

extern spec for slice<T>::split_at_mut

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

ghost

requires 

self

ensures 

self

ensures 

self

ensures 

self

ensures 

(^result.0)@ == (^self)@[..mid@]

ensures 

(^result.1)@ == (^self)@[mid@..]