Makes rndFin take all values in Fin (S k)
Previously, rndFin k only took values in 0, 1, ... , k - 1, even
though the type Fin (S k) has elements 0, 1, ..., k.
commitce9afaedc7f424fa4e077f04fb7c145b69439297
authorKester Tong <kestert@google.com>
dateSat 26 Apr 2014, 00:55 (13 years ago)
parent7ed177a
libs/effects/Effect/Random.idr+1−1
@@ -21,7 +21,7 @@ rndInt lower upper = do v <- getRandom
2121 return (v `prim__sremBigInt` (upper - lower) + lower)
2222
2323rndFin : (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))
2525 return (toFin v)
2626 where toFin : Integer -> Fin (S k)
2727 toFin x = case integerToFin x (S k) of