vstd/arithmetic: broadcast power2 lemmas

verus-lang / verus

Verified Rust for low-level systems code

MIT License

1.15k stars 66 forks source link

Closed mmcloughlin closed 4 months ago

mmcloughlin commented 4 months ago

Replace the *_auto lemmas in vstd::arithmetic::power2 with broadcast versions.

Along the way, this PR also removes unused imports in the power2 module.

Updates #1118