lean4-htt/tests/playground/rand.lean
Leonardo de Moura 8db0474571 feat(library/init/data/random): random numbers
It is useful for creating tests.
2019-05-04 15:57:42 -07:00

4 lines
196 B
Text

def main (xs : List String) : IO Unit :=
do [seed, n] ← pure (xs.map String.toNat) | throw "invalid number of arguments",
IO.setRandSeed seed,
n.mfor $ λ _, IO.rand 0 1000 >>= IO.println