pub open spec fn lift_action<T>(action_pred: ActionPred<T>) -> TempPred<T>Expand description
{ TempPred::new(|ex: Execution<T>| action_pred.apply(ex.head(), ex.head_next())) }pub open spec fn lift_action<T>(action_pred: ActionPred<T>) -> TempPred<T>{ TempPred::new(|ex: Execution<T>| action_pred.apply(ex.head(), ex.head_next())) }