Function vstd::std_specs::vec::ex_vec_pop

source · 
pub exec fn ex_vec_pop<T, A: Allocator>(vec: &mut Vec<T, A>) -> Option<T>
Expand description
ensures
old(vec)@.len() > 0
    ==> value == Some(old(vec)@[old(vec)@.len() - 1])
        && vec@ == old(vec)@.subrange(0, old(vec)@.len() - 1),
old(vec)@.len() == 0 ==> value == None::<T> && vec@ == old(vec)@,