From 4600bb16fcded0356d20ae232e7f8580c56a5955 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Tue, 19 Nov 2024 00:26:03 -0500 Subject: [PATCH] feat: use `BaseIO` at `IO.rand` (#6102) This PR moves `IO.rand` and `IO.setRandSeed` to be in the `BaseIO` monad. This is their proper monad as neither can error. --- src/Init/Data/Random.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Random.lean b/src/Init/Data/Random.lean index b5475ba9d7..42ef42c7f3 100644 --- a/src/Init/Data/Random.lean +++ b/src/Init/Data/Random.lean @@ -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