@@ -32,14 +32,14 @@ rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))
32 Just v => v
32 Just v => v
33 Nothing => toFin (assert_smaller x (x - cast (S k)))
33 Nothing => toFin (assert_smaller x (x - cast (S k)))
35−||| Select a random element from a vector, or Nothing if the vector is empty
35+||| Select a random element from a vector
36−rndSelect' : Vect n a -> { [RND] } Eff IO (Maybe a)
36+rndSelect' : Vect (S k) a -> { [RND] } Eff IO a
37−rndSelect' {n=Z} _ = return Nothing
38−rndSelect' {n=(S k)} xs = return (Just (Vect.index !(rndFin k) xs))
37+rndSelect' {k} xs = return (Vect.index !(rndFin k) xs)
40||| Select a random element from a list, or Nothing if the list is empty
39||| Select a random element from a list, or Nothing if the list is empty
41rndSelect : List a -> { [RND] } Eff IO (Maybe a)
40rndSelect : List a -> { [RND] } Eff IO (Maybe a)
41+rndSelect [] = return Nothing
42−rndSelect l = rndSelect' (fromList l)
42+rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))
44||| Sets the random seed
44||| Sets the random seed
45srand : Integer -> { [RND] } Eff m ()
45srand : Integer -> { [RND] } Eff m ()