add Problem 21

Src.lean

@@ -11,6 +11,7 @@ import Src.Problem18
 import Src.Problem19
 import Src.Problem2
 import Src.Problem20
+import Src.Problem21
 import Src.Problem3
 import Src.Problem31
 import Src.Problem32

Src/Problem21.lean

@@ -0,0 +1,18 @@
+/-
+# Problem 21
+Insert an element at a given position into a list.
+-/
+variable {α : Type}
+
+def insertAt (e : α) (l : List α) (i : Nat) : List α :=
+  -- sorry
+  l.take (i - 1) ++ [e] ++ l.drop (i - 1)
+  -- sorry
+
+-- The following code is a test case and you should not change it.
+
+example : insertAt "X" ["1", "2", "3", "4"] 2 = ["1", "X", "2", "3", "4"] := rfl
+
+example : insertAt "X" ["1", "2", "3", "4"] 1 = ["X", "1", "2", "3", "4"] := rfl
+
+example : insertAt "X" [] 1 = ["X"] := rfl

md/SUMMARY.md

@@ -28,6 +28,10 @@
 * [19: Rotate a list](./build/Problem19.md)
 * [20: Remove the K'th element](./build/Problem20.md)
 
+# 21-30: Lists again
+
+* [21: Insert an element](./build/Problem21.md)
+
 # 31-40: Arithmetic
 
 * [31: Prime number detection](./build/Problem31.md)