fix: Selectable.one does not panic on empty array (#10216)

This PR fixes #10193.
This commit is contained in:
Henrik Böving 2025-09-02 13:55:36 +02:00 committed by GitHub
parent 96c42b95fa
commit c5f2c192d6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 8 additions and 0 deletions

View file

@ -123,6 +123,9 @@ The protocol for this is as follows:
the `Selectable.cont` of the winning `Selector` is executed and returned.
-/
partial def Selectable.one (selectables : Array (Selectable α)) : IO (AsyncTask α) := do
if selectables.isEmpty then
throw <| .userError "Selectable.one requires at least one Selectable"
let seed := UInt64.toNat (ByteArray.toUInt64LE! (← IO.getRandomBytes 8))
let gen := mkStdGen seed
let selectables := shuffleIt selectables gen

View file

@ -27,3 +27,8 @@ def test2 : IO (AsyncTask Nat) := do
#eval show IO _ from do
let task ← test2
IO.ofExcept task.get
/-- error: Selectable.one requires at least one Selectable -/
#guard_msgs in
#eval show IO _ from do
let foo ← Selectable.one (α := Unit) #[]