Function extern_spec_T__slice_T_swap 

pub fn extern_spec_T__slice_T_swap<T>(self_: &mut [T], i: usize, j: usize)

extern spec for slice<T>::swap

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

terminates

ghost

requires

i@ < self@.len()

requires

j@ < self@.len()

ensures

(^self)@.exchange(self@, i@, j@)