extern_spec_T_PartialEq_Option_T_eq

creusot_contracts::std::option

Function extern_spec_T_PartialEq_Option_T_eq 

Source 
pub fn extern_spec_T_PartialEq_Option_T_eq<T: PartialEq + DeepModel>(
    self_: &Option<T>,
    rhs: &Option<T>,
) -> bool
Expand description

extern spec for Option<T>::eq

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

ensures 

result == (self.deep_model() == rhs.deep_model())