Random
📁 Source: Mathlib/Control/Random.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsBoundedRandom, randomR, runRand, runRandWith, Rand, next, range, split, RandG, RandGT, RandT, Random, instBool, instBoundedRandomFin, instBoundedRandomInt, instBoundedRandomNat, instBoundedRandomULiftOfULiftableOfMonad, instFinOfNeZeroNat, instULiftOfULiftable, rand, randBool, randBound, randFin, instMonadLiftTRandGTOfMonadLift | 24 |
| Theorems | 0 |
| Total | 24 |
BoundedRandom
Definitions
| Name | Category | Theorems |
|---|---|---|
randomR 📖 | CompOp | — |
IO
Definitions
| Name | Category | Theorems |
|---|---|---|
runRand 📖 | CompOp | — |
runRandWith 📖 | CompOp | — |
Rand
Definitions
| Name | Category | Theorems |
|---|---|---|
next 📖 | CompOp | — |
range 📖 | CompOp | — |
split 📖 | CompOp | — |
Random
Definitions
| Name | Category | Theorems |
|---|---|---|
instBool 📖 | CompOp | — |
instBoundedRandomFin 📖 | CompOp | — |
instBoundedRandomInt 📖 | CompOp | — |
instBoundedRandomNat 📖 | CompOp | — |
instBoundedRandomULiftOfULiftableOfMonad 📖 | CompOp | — |
instFinOfNeZeroNat 📖 | CompOp | — |
instULiftOfULiftable 📖 | CompOp | — |
rand 📖 | CompOp | — |
randBool 📖 | CompOp | — |
randBound 📖 | CompOp | — |
randFin 📖 | CompOp | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
BoundedRandom 📖 | CompData | — |
Rand 📖 | CompOp | — |
RandG 📖 | CompOp | — |
RandGT 📖 | CompOp | — |
RandT 📖 | CompOp | — |
Random 📖 | CompData | — |
instMonadLiftTRandGTOfMonadLift 📖 | CompOp | — |
---