git.iko.soy/Idris-dev
on master help sign in
Makes rndFin take all values in Fin (S k)
ce9afaeKester Tong
libs/effects/Effect/Random.idr+1−1
compare with master
unifiedsplit
@@ -21,7 +21,7 @@ rndInt lower upper = do v <- getRandom
21 return (v `prim__sremBigInt` (upper - lower) + lower)
21 return (v `prim__sremBigInt` (upper - lower) + lower)
22
22
23rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
23rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))
24−rndFin k = do let v = !getRandom `prim__sremBigInt` (cast k)
24+rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))
25 return (toFin v)
25 return (toFin v)
26 where toFin : Integer -> Fin (S k)
26 where toFin : Integer -> Fin (S k)
27 toFin x = case integerToFin x (S k) of
27 toFin x = case integerToFin x (S k) of