vstd::arithmetic

Module power

Source
Expand description

This file contains proofs related to exponentiation. 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/Power.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§