| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| | |
The standard library uses Z.*, and Z* and Z_* are compatibility
notations. We follow suit.
Also, eliminate a few lemmas that are duplicates of ones in the standard
library.
|
|/
|
|
| |
than sticking the value of the Z input in the first digit. The condition that c is positive has been added to PseudoMersenneBaseParams--it is necessary for this encode and for canonicalization, for which it was previously a section variable.
|
|
|
|
|
| |
This prevents notation conflicts (see comment in Notations.v for more
explanation).
|
|
|
|
| |
length of the base vector
|
|\ |
|
| | |
|
|/ |
|
|
|
|
| |
general contexts.
|
|
organization and changes to pseudomersenne base parameters that require bases to be expressed as powers of 2, which reduces the burden of proof on the caller and allows carry functions to use bitwise operations rather than mod and division
|