Module vstd::arithmetic::logarithm
source · Expand description
This file contains proofs related to integer logarithms. 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/Logarithm.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 *******************************************************************************/