implies_new_invariant_n_internal

vstd_extra

Macro implies_new_invariant_n_internal 

Source 
macro_rules! implies_new_invariant_n_internal {
    ($spec:expr, $init:expr, $next:expr, $inv:expr, $p1:expr) => { ... };
    ($spec:expr, $init:expr, $next:expr, $inv:expr, $p1:expr,) => { ... };
    ($spec:expr, $init:expr, $next:expr, $inv:expr, $($preds:expr),+) => { ... };
    ($spec:expr, $init:expr, $next:expr, $inv:expr, $($preds:expr),+ ,) => { ... };
}