Module vstd::arithmetic::mul
source · Expand description
This file contains proofs related to integer multiplication (*).
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/Mul.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 *******************************************************************************/