Function extern_spec_std_mem_take 

pub fn extern_spec_std_mem_take<T: Default>(dest: &mut T) -> T

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

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

ensures

result == *dest

ensures

T::default.postcondition((), ^dest)