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