extern_spec_Add_Duration_Instant_add

creusot_contracts::std::time

Function extern_spec_Add_Duration_Instant_add 

Source 
pub fn extern_spec_Add_Duration_Instant_add(
    self_: Instant,
    rhs: Duration,
) -> Instant
Expand description

extern spec for Instant::add

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

terminates

ghost

ensures 

rhs@ == 0 ==> self@ == result@

ensures 

rhs@ > 0 ==> self@ < result@