Skip to content

Commit

Permalink
feat: use BaseIO at IO.rand (#6102)
Browse files Browse the repository at this point in the history
This PR moves `IO.rand` and `IO.setRandSeed` to be in the `BaseIO`
monad.

This is their proper monad as neither can error.
  • Loading branch information
tydeu authored Nov 19, 2024
1 parent 7ccdfc3 commit 4600bb1
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Init/Data/Random.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 4600bb1

Please sign in to comment.