Q20

Src.lean

@@ -5,6 +5,7 @@ import Src.Problem12
 import Src.Problem14
 import Src.Problem15
 import Src.Problem2
+import Src.Problem20
 import Src.Problem3
 import Src.Problem31
 import Src.Problem32

Src/Problem20.lean

@@ -0,0 +1,25 @@
+/-
+  # Problem 20
+  Remove the K'th element from a list.
+-/
+variable {α : Type}
+
+def removeAt (l : List α) (n : Nat) : List α :=
+  -- sorry
+  match l,n with
+  | [] , _ => []
+  | _ , 0 => l
+  | x :: b , m + 2 => x :: removeAt b (m+1)
+  | _ :: b , _ => b
+  -- sorry
+
+-- The following code is a test case and you should not change it.
+example : removeAt ['a','b','c','d'] 2 = ['a','c','d'] := rfl
+
+example : removeAt ['a','b','c','d'] 5 = ['a','b','c','d'] := rfl
+
+example : removeAt ['a','b','c','d'] 0 = ['a','b','c','d'] := rfl
+
+example : removeAt ['a'] 1 = [] := rfl
+
+example : removeAt ([] : List α) 1 = [] := rfl

md/SUMMARY.md

@@ -21,6 +21,7 @@
 * [12: Decode a run-length encoded list](./build/Problem12.md)
 * [14: Duplicate elements](./build/Problem14.md)
 * [15: Replicate elements K times](./build/Problem15.md)
+* [20: Remove the K'th element](./build/Problem20.md)
 
 # 31-40: Arithmetic