Module vstd::arithmetic::power2

source ·
Expand description

This file contains proofs related to powers of 2. These are part of the math standard library.

It’s based on the following file from the Dafny math standard library: Source/DafnyStandardLibraries/src/Std/Arithmetic/Power2.dfy. That file has the following copyright notice: /*******************************************************************************

  • Original: Copyright (c) Microsoft Corporation
  • SPDX-License-Identifier: MIT
  • Modifications and Extensions: Copyright by the contributors to the Dafny Project
  • SPDX-License-Identifier: MIT *******************************************************************************/

Functions§