lift_state

vstd_extra::temporal_logic::defs

Function lift_state 

Source 
pub open spec fn lift_state<T>(state_pred: StatePred<T>) -> TempPred<T>
Expand description
{ TempPred::new(|ex: Execution<T>| state_pred.apply(ex.head())) }