Function extern_spec_core_cmp_Ord_min 

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

extern spec for ::core::cmp::Ord::min

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.deep_model() < o.deep_model() ==> result == self

ensures

self