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