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