Function extern_spec_std_mem_swap 

pub fn extern_spec_std_mem_swap<T>(x: &mut T, y: &mut T)

extern spec for ::std::mem::swap<T>

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

terminates

ghost

ensures

^x == *y

ensures

^y == *x