@@ -16,10 +16,14 @@ using (m : Type -> Type)
1616RND : EFFECT
1717RND = MkEff Integer Random
1818
19+||| Generates a random Integer in a given range
1920rndInt : Integer -> Integer -> { [RND] } Eff m Integer
2021rndInt lower upper = do v <- getRandom
2122 return (v `prim__sremBigInt` (upper - lower) + lower)
2223
24+||| Generate a random number in Fin (S `k`)
25+|||
26+||| Note that rndFin k takes values 0, 1, ..., k.
2327rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
2428rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))
2529 return (toFin v)
@@ -28,6 +32,7 @@ rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))
2832 Just v => v
2933 Nothing => toFin (assert_smaller x (x - cast (S k)))
3034
35+||| Sets the random seed
3136srand : Integer -> { [RND] } Eff m ()
3237srand n = setSeed n
3338