extern_spec_std_ops_Idx_RangeInclusive_Idx_end

creusot_contracts::std::ops

Function extern_spec_std_ops_Idx_RangeInclusive_Idx_end 

Source 
pub fn extern_spec_std_ops_Idx_RangeInclusive_Idx_end<Idx>(
    self_: &RangeInclusive<Idx>,
) -> &Idx
Expand description

extern spec for ::std::ops::RangeInclusive<Idx>::end

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

ensures 

*result == self.end_log()