pub open spec fn enabled<T>(action_pred: ActionPred<T>) -> StatePred<T>Expand description
{ StatePred::new(|s: T| exists |s_prime: T| #[trigger] action_pred.apply(s, s_prime)) }pub open spec fn enabled<T>(action_pred: ActionPred<T>) -> StatePred<T>{ StatePred::new(|s: T| exists |s_prime: T| #[trigger] action_pred.apply(s, s_prime)) }