Function extern_spec_T_A_From_Vec_T_A_Box__slice_T_A_from 

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

extern spec for Box<slice<T>, A>::from

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

ghost

ensures

result@ == v@