Function vstd::std_specs::option::ex_option_clone

source · 
pub exec fn ex_option_clone<T: Clone>(opt: &Option<T>) -> res : Option<T>
Expand description
ensures
opt.is_none() ==> res.is_none(),
opt.is_some() ==> res.is_some() && call_ensures(T::clone, (&opt.unwrap(),), res.unwrap()),