pub open spec fn tla_forall<T, A>(
a_to_temp_pred: FnSpec<(A,), TempPred<T>>,
) -> TempPred<T>Expand description
{
TempPred::new(|ex: Execution<T>| {
forall |a: A| #[trigger] a_to_temp_pred(a).satisfied_by(ex)
})
}\A for temporal predicates in TLA+ (i.e., forall in Verus).