Function vstd::std_specs::option::ex_map

source · 
pub exec fn ex_map<T, U, F: FnOnce(T) -> U>(a: Option<T>, f: F) -> ret : Option<U>
Expand description
requires
a.is_some() ==> f.requires((a.unwrap(),)),
ensures
ret.is_some() == a.is_some(),
ret.is_some() ==> f.ensures((a.unwrap(),), ret.unwrap()),