Function vstd::std_specs::option::as_ref

source · 
pub exec fn as_ref<T>(option: &Option<T>) -> a : Option<&T>
Expand description
ensures
a.is_Some() <==> option.is_Some(),
a.is_Some() ==> option.get_Some_0() == a.get_Some_0(),