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