Macro vstd::assert_by_contradiction

source ·
macro_rules! assert_by_contradiction {
    ($($a:tt)*) => { ... };
}
Expand description

Allows you to prove a boolean predicate by assuming its negation and proving a contradiction.

assert_by_contradiction!(b, { /* proof */ }); Equivalent to writing if !b { /* proof */; assert(false); } but is more concise and documents intent.

assert_by_contradiction!(b, {
    // assume !b here
    // prove `false`
});