MersenneTwister
📁 Source: Batteries/Data/Random/MersenneTwister.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsConfig, init, initMult, initSeed, maskBits, shiftSize, stateSize, temperingMasks, temperingShifts, wordSize, xorMask, State, data, index, next, twist, update, instStreamStateBitVecWordSize, mt19937, mt19937_64 | 20 |
| 2 | |
| Total | 22 |
Batteries.Random.MersenneTwister
Definitions
| Name | Category | Theorems |
|---|---|---|
Config 📖 | CompData | — |
State 📖 | CompData | — |
instStreamStateBitVecWordSize 📖 | CompOp | — |
mt19937 📖 | CompOp | — |
mt19937_64 📖 | CompOp | — |
Batteries.Random.MersenneTwister.Config
Definitions
| Name | Category | Theorems |
|---|---|---|
init 📖 | CompOp | — |
initMult 📖 | CompOp | — |
initSeed 📖 | CompOp | — |
maskBits 📖 | CompOp | — |
shiftSize 📖 | CompOp | — |
stateSize 📖 | CompOp | |
temperingMasks 📖 | CompOp | — |
temperingShifts 📖 | CompOp | — |
wordSize 📖 | CompOp | |
xorMask 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
zero_lt_stateSize 📖 | mathematical | — | stateSize | — | — |
zero_lt_wordSize 📖 | mathematical | — | wordSize | — | — |
Batteries.Random.MersenneTwister.State
Definitions
| Name | Category | Theorems |
|---|---|---|
data 📖 | CompOp | — |
index 📖 | CompOp | — |
next 📖 | CompOp | — |
twist 📖 | CompOp | — |
update 📖 | CompOp | — |
---