Function extern_spec_Idx_RangeInclusive_Idx_end 

pub fn extern_spec_Idx_RangeInclusive_Idx_end<Idx>(
    self_: &RangeInclusive<Idx>,
) -> &Idx

extern spec for RangeInclusive<Idx>::end

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

ensures

*result == self.end_log()