@@ -20,6 +20,14 @@ rndInt : Integer -> Integer -> { [RND] } Eff m Integer
20rndInt lower upper = do v <- getRandom
20rndInt lower upper = do v <- getRandom
21 return (v `prim__sremBigInt` (upper - lower) + lower)
21 return (v `prim__sremBigInt` (upper - lower) + lower)
23+rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
24+rndFin k = do let v = !getRandom `prim__sremBigInt` (cast k)
26+ where toFin : Integer -> Fin (S k)
27+ toFin x = case integerToFin x (S k) of
29+ Nothing => toFin (assert_smaller x (x - cast (S k)))
23srand : Integer -> { [RND] } Eff m ()
31srand : Integer -> { [RND] } Eff m ()
24srand n = setSeed n
32srand n = setSeed n