Function extern_spec_T_U_AsRef_U__ref_T_as_ref 

pub fn extern_spec_T_U_AsRef_U__ref_T_as_ref<'a, 'b, T, U: ?Sized>(
    self_: &'b &'a T,
) -> &'b U
where
    T: AsRef<U> + ?Sized,

extern spec for <&T as AsRef<U>>::as_ref

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

requires

<T as AsRef<U>>::as_ref.precondition((*self,))

ensures

<T as AsRef<U>>::as_ref.postcondition((*self,), result)