Function extern_spec_T__slice_T_into_vec 

pub fn extern_spec_T__slice_T_into_vec<T, A: Allocator>(
    self_: Box<[T], A>,
) -> Vec<T, A>

extern spec for slice<T>::into_vec

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

ghost

ensures

result@ == self_@