always

vstd_extra::temporal_logic::defs

Function always 

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