Function extern_spec_T_E_Result_T_E_as_ref 

pub fn extern_spec_T_E_Result_T_E_as_ref<T, E>(
    self_: &Result<T, E>,
) -> Result<&T, &E>

extern spec for Result<T, E>::as_ref

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

terminates

ghost

ensures

forall<t: &T> *self == Ok(*t) ==> result == Ok(t)

ensures

forall<e: &E> *self == Err(*e) ==> result == Err(e)