not

vstd_extra::temporal_logic::defs

Function not 

Source 
pub open spec fn not<T>(temp_pred: TempPred<T>) -> TempPred<T>
Expand description
{ TempPred::new(|ex: Execution<T>| !temp_pred.satisfied_by(ex)) }

~ for temporal predicates in TLA+ (i.e., ! in Verus).