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`
});