kani

Macro implies

Source
macro_rules! implies {
    ($premise:expr => $conclusion:expr) => { ... };
}
Expand description

implies!(premise => conclusion) means that if the premise is true, so must be the conclusion.

This simply expands to !premise || conclusion and is intended to make checks more readable, as the concept of an implication is more natural to think about than its expansion.