Problem 23

(Intermediate 🌟🌟) Extract a given number of randomly selected elements from a list.

import Lean

variable {α : Type} [Inhabited α]

def rndSelect (l : List α) (n : Nat) : IO (List α) := do
  sorry

-- The following codes are for test and you should not edit these.

def runTest [BEq α] [ToString α] (l : List α) (n : Nat) : IO Unit := do
  let result ← rndSelect l n
  let check := result.length == n
    |> (· && result.all l.contains)
  if check then
    IO.println s!"ok!"
  else
    throw <| .userError s!"failed: rndSelect {l} {n} = {result}"

#eval runTest [1, 2, 3] 0

#eval runTest ['a', 'b'] 1

#eval runTest [1, 2, 3, 4, 5] 2

#eval runTest [1, 1, 1] 2

#eval runTest [2, 2, 2] 12

#eval runTest (List.range 5200) 1897