commit: 4600bb16fcded0356d20ae232e7f8580c56a5955

[log]
author: Mac Malone <tydeu@hatpress.net>

Tue Nov 19 00:26:03 2024 -0500
committer: GitHub <noreply@github.com>

Tue Nov 19 05:26:03 2024 +0000
tree: 9c2757cdb9b1eed68023ca87899d395176dfa49d
parent: 7ccdfc30ffab9ad2059d89aa03627fd549e4e7f4 [diff]

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[diff]

1 file changed

tree: 9c2757cdb9b1eed68023ca87899d395176dfa49d

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).