Function extern_spec_T_A_Vec_T_A_pop 

pub fn extern_spec_T_A_Vec_T_A_pop<T, A: Allocator>(
    self_: &mut Vec<T, A>,
) -> Option<T>

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

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

terminates

ghost

ensures

match result {
    Some(t) =>
        (^self)@ == self@.subsequence(0, self@.len() - 1) &&
        self@ == (^self)@.push_back(t),
    None => *self == ^self && self@.len() == 0
}