IdrisGL.Random

Definitions

randomInt : Int -> Int -> Int

  An unsafe, predictable and limited random integer generator, in range [lower, upper].
  Switch <lower> and <upper> if <upper> is LOWER than <lower>.
  
  This function is only for users who want to easily render random picture elements.
  Please don't use it for precise calculations.
  No random built-in functions been found in idris2 version 0.4.
  
  @ lower Lower bound.
  @ upper Upper bound.

Visibility: export

randomNat : Nat -> Nat -> Nat

  An unsafe, predictable and limited random natrual number generator, in range [lower, upper].
  Switch <lower> and <upper> if <upper> is LOWER than <lower>.
  
  This function is only for users who want to easily render random picture elements.
  Please don't use it for precise calculations.
  No random built-in functions been found in idris2 version 0.4.
  
  @ lower Lower bound.
  @ upper Upper bound.

Visibility: export

randomFin : Nat -> (upper : Nat) -> Maybe (Fin upper)

  An unsafe, predictable and limited random (Fin upper) generator, in range [lower, upper].
  Switch <lower> and <upper> if <upper> is LOWER than <lower>.
  
  This function is only for users who want to easily render random picture elements.
  Please don't use it for precise calculations.
  No random built-in functions been found in idris2 version 0.4.
  
  @ lower Lower bound.
  @ upper Upper bound.

Visibility: export

randomPick : List a -> Maybe a

Visibility: export