extern_spec_std_ops_Idx_RangeInclusive_Idx_start

creusot_contracts::std::ops

Function extern_spec_std_ops_Idx_RangeInclusive_Idx_start 

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

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

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

ensures 

*result == self.start_log()