lift_state_prime

vstd_extra::temporal_logic::defs

Function lift_state_prime 

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