@@ -21,7 +21,7 @@ rndInt : (rnd : Var) -> Integer -> Integer -> ST m Integer [rnd ::: Random]
2121rndInt rnd lower upper = do v <- getRandom rnd
2222 pure $ assert_total ((v `prim__sremBigInt` (upper - lower)) + lower)
2323
24−||| Generate a random number in Fin (S `k`)
24+||| Generate a random number in `Fin (S k)`
2525|||
2626||| Note that rndFin k takes values 0, 1, ..., k.
2727rndFin : (rnd : Var) -> (k : Nat) -> ST m (Fin (S k)) [rnd ::: Random]
@@ -36,7 +36,7 @@ rndFin rnd k = do let v = assert_total $ !(getRandom rnd) `prim__sremBigInt` (ca
3636rndSelect' : (rnd : Var) -> Vect (S k) a -> ST m a [rnd ::: Random]
3737rndSelect' {k} rnd xs = pure (Vect.index !(rndFin rnd k) xs)
3838
39−||| Select a random element from a list, or Nothing if the list is empty
40−rndSelect : (rnd : Var) -> List a -> ST m (Maybe a) [rnd ::: Random]
41−rndSelect rnd [] = pure Nothing
42−rndSelect rnd (x::xs) = pure (Just !(rndSelect' rnd (x::(fromList xs))))
39+||| Select a random element from a non-empty list
40+rndSelect : (rnd : Var) -> (xs : List a) -> {auto ok : NonEmpty xs} -> ST m a [rnd ::: Random]
41+rndSelect rnd (x::xs) {ok=NonEmpty} = pure ( !(rndSelect' rnd (x::(fromList xs))))
42+rndSelect rnd [] {ok=NonEmpty} impossible