always_lift_state_weaken_n_internal

vstd_extra

Macro always_lift_state_weaken_n_internal 

Source 
macro_rules! always_lift_state_weaken_n_internal {
    ($spec:expr, $p1:expr, $h:expr) => { ... };
    ($spec:expr, $p1:expr, $p2:expr, $h:expr) => { ... };
    ($spec:expr, $p1:expr, $p2:expr, $h:expr,) => { ... };
    ($spec:expr, $p1:expr, $p2:expr, $($tail:expr),+ , $h:expr) => { ... };
    ($spec:expr, $p1:expr, $p2:expr, $($tail:expr),+ , $h:expr,) => { ... };
}