Lean 4 (Meta)programming Cookbook

Get a Random Number🔗

You can get a random number with lower low and upper high bounds using the IO.rand function.

def getRandomNumber (low high : Nat) : IO Unit := do let random IO.rand low high IO.println s!"Random number between {low} and {high}: {random}"