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.

ghost

requires

self

requires

self

ensures

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