add P23: WIP

without test cases

Src.lean

@@ -13,6 +13,7 @@ import Src.Problem2
 import Src.Problem20
 import Src.Problem21
 import Src.Problem22
+import Src.Problem23
 import Src.Problem3
 import Src.Problem31
 import Src.Problem32

Src/Problem23.lean

@@ -0,0 +1,16 @@
+/-
+# Problem 23
+Extract a given number of randomly selected elements from a list.
+-/
+variable {α : Type} [Inhabited α]
+
+def rndSelect (l : List α) (n : Nat) : IO (List α) := do
+  -- sorry
+  match l, n with
+  | [], _ => pure []
+  | _, 0 => pure []
+  | _, n + 1 =>
+    let index ← IO.rand 0 $ l.length - 1
+    let previous ← rndSelect l n
+    pure <| l[index]! :: previous
+  -- sorry

md/SUMMARY.md

@@ -32,6 +32,7 @@
 
 * [21: Insert an element](./build/Problem21.md)
 * [22: Integers within a range](./build/Problem22.md)
+* [23: Random selection](./build/Problem23.md)
 
 # 31-40: Arithmetic