max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: use BaseIO at IO.rand (#6102)

Browse source 
This PR moves `IO.rand` and `IO.setRandSeed` to be in the `BaseIO`
monad.

This is their proper monad as neither can error.
This commit is contained in:
Mac Malone 2024-11-19 00:26:03 -05:00 • committed by GitHub
parent 7ccdfc30ff
commit 4600bb16fc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Data/Random.lean
View file

@ -113,10 +113,10 @@ initialize IO.stdGenRef : IO.Ref StdGen ←
let seed := UInt64.toNat (ByteArray.toUInt64LE! (← IO.getRandomBytes 8))
IO.mkRef (mkStdGen seed)
def IO.setRandSeed (n : Nat) : IO Unit :=
def IO.setRandSeed (n : Nat) : BaseIO Unit :=
IO.stdGenRef.set (mkStdGen n)
def IO.rand (lo hi : Nat) : IO Nat := do
def IO.rand (lo hi : Nat) : BaseIO Nat := do
let gen ← IO.stdGenRef.get
let (r, gen) := randNat gen lo hi
IO.stdGenRef.set gen