Function vstd::std_specs::vec::ex_vec_pop

pub exec fn ex_vec_pop<T, A: Allocator>(vec: &mut Vec<T, A>) -> value : 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)@,