eventually

vstd_extra::temporal_logic::defs

Function eventually 

Source 
pub open spec fn eventually<T>(temp_pred: TempPred<T>) -> TempPred<T>
Expand description
{
    TempPred::new(|ex: Execution<T>| {
        exists |i: nat| #[trigger] temp_pred.satisfied_by(ex.suffix(i))
    })
}