Lean 4(元)编程 Cookbook

获取一个随机数🔗

你可以使用 IO.rand 函数获取一个下界为 low、上界为 high 的随机数。

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