diff --git a/src/Std/Internal/Async/Select.lean b/src/Std/Internal/Async/Select.lean index b893d86825..ebbb51d48d 100644 --- a/src/Std/Internal/Async/Select.lean +++ b/src/Std/Internal/Async/Select.lean @@ -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 diff --git a/tests/lean/run/async_select_timer.lean b/tests/lean/run/async_select_timer.lean index ecb2232825..7999798c7b 100644 --- a/tests/lean/run/async_select_timer.lean +++ b/tests/lean/run/async_select_timer.lean @@ -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) #[]