Function extern_spec_std_cmp_Ord_clamp 

pub fn extern_spec_std_cmp_Ord_clamp<Self_>(
    self_: Self_,
    min: Self_,
    max: Self_,
) -> Self_
where
    Self_: Sized + DeepModel + ?Sized + Ord,
    Self_::DeepModelTy: OrdLogic,

extern spec for ::std::cmp::Ord::clamp

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

requires

min.deep_model() <= max.deep_model()

ensures

result.deep_model() >= min.deep_model()

ensures

result.deep_model() <= max.deep_model()

ensures

result == self || result == min || result == max

ensures

if self.deep_model() > max.deep_model() {
                    result == max
                } else if self.deep_model() < min.deep_model() {
                    result == min
                } else { result == self }