Function extern_spec_core_cmp_max 

pub fn extern_spec_core_cmp_max<T: Ord + DeepModel<DeepModelTy: OrdLogic>>(
    v1: T,
    v2: T,
) -> T

extern spec for ::core::cmp::max<T>

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

ensures

result.deep_model() >= v1.deep_model()

ensures

result.deep_model() >= v2.deep_model()

ensures

result == v1 || result == v2

ensures

v1.deep_model() <= v2.deep_model() ==> result == v2

ensures

v2.deep_model() < v1.deep_model() ==> result == v1