Function extern_spec_T_A_Vec_T_A_remove 

pub fn extern_spec_T_A_Vec_T_A_remove<T, A: Allocator>(
    self_: &mut Vec<T, A>,
    ix: usize,
) -> T

extern spec for Vec<T, A>::remove

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

terminates

ghost

requires

ix@ < self@.len()

ensures

result == self[ix@]

ensures

(^self)@ == self@.subsequence(0, ix@).concat(self@.subsequence(ix@ + 1, self@.len()))

ensures

(^self)@.len() == self@.len() - 1