Function extern_spec_T_Option_T_take_if 

pub fn extern_spec_T_Option_T_take_if<T, P: FnOnce(&mut T) -> bool>(
    self_: &mut Option<T>,
    predicate: P,
) -> Option<T>

extern spec for Option<T>::take_if

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

requires

match *self {
    None => true,
    Some(t) => forall<b:&mut T> inv(b) && *b == t ==> predicate.precondition((b,)),
}

ensures

match *self {
    None => result == None && ^self == None,
    Some(cur) =>
        exists<b: &mut T, res: bool> inv(b) && cur == *b && predicate.postcondition_once((b,), res) &&
            if res {
                ^self == None && result == Some(^b)
            } else {
                ^self == Some(^b) && result == None
            }
}