Function extern_spec_T_Option_T_as_deref 

pub fn extern_spec_T_Option_T_as_deref<T>(
    self_: &Option<T>,
) -> Option<&<T as Deref>::Target>
where
    T: Deref,

extern spec for Option<T>::as_deref

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

requires

match self {
    None => true,
    Some(x) => T::deref.precondition((x,)),
}

ensures

match (self, result) {
    (None, None) => true,
    (Some(x), Some(r)) => T::deref.postcondition((x,), r),
    _ => false,
}