Function extern_spec_core_cmp_Ord_max 

pub fn extern_spec_core_cmp_Ord_max<Self_>(self_: Self_, o: Self_) -> Self_
where
    Self_: Sized + ?Sized + Ord + DeepModel<DeepModelTy: OrdLogic>,

extern spec for ::core::cmp::Ord::max

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

ensures

self

ensures

result.deep_model() >= o.deep_model()

ensures

self

ensures

self

ensures

self.deep_model() ==> result == self