later

vstd_extra::temporal_logic::defs

Function later 

Source 
pub open spec fn later<T>(temp_pred: TempPred<T>) -> TempPred<T>
Expand description
{ TempPred::new(|ex: Execution<T>| temp_pred.satisfied_by(ex.suffix(1))) }