fix: Selectable.one does not panic on empty array

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

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) #[]