Create Some file

Src.lean

@@ -1,3 +1,5 @@
 import Src.Problem1
 import Src.Problem2
+import Src.Problem3
+import Src.Problem4
 import Src.README

Src/Problem3.lean

@@ -0,0 +1,28 @@
+/-
+# Problem 3
+Find the K'th element of a list.
+-/
+
+variable {α : Type}
+
+def elementAt (l : List α) (k : Nat) : Option α :=
+  -- sorry
+  match k, l with
+  | _, [] => none
+  | 0, _ => none
+  | 1, [a] => some a
+  | 1, a :: _ => some a
+  | Nat.succ k, _ :: a => elementAt a k
+  -- sorry
+
+-- The following is a test case, you don't need to edit it.
+
+example : elementAt ['a', 'b', 'c', 'd', 'e'] 3 = some 'c' := by rfl
+
+example : elementAt ['a', 'b', 'c', 'd', 'e'] 6 = none := by rfl
+
+example : elementAt ['a', 'b', 'c', 'd', 'e'] 0 = none := by rfl
+
+example : elementAt ([] : List α) 0 = none := by rfl
+
+example : elementAt [1, 2, 3] 2 = some 2 := by rfl

Src/Problem4.lean

@@ -0,0 +1,24 @@
+/-
+# Problem 4
+Find the number of elements in a list.
+-/
+
+variable {α : Type}
+
+def myLength (l : List α) : Nat :=
+  -- sorry
+  match l with
+  | [] => 0
+  | [_] => 1
+  | _ :: a => (myLength a).succ
+  -- sorry
+
+-- The following is a test case, you don't need to edit it.
+
+example : myLength [123, 456, 789] = 3 := by rfl
+
+example : myLength ['L', 'e', 'a', 'n', '4'] = 5 := by rfl
+
+example : myLength [False, True, True] = 3 := by rfl
+
+example : myLength ([] : List α) = 0 := by rfl

md/SUMMARY.md

@@ -6,4 +6,8 @@
 
 * [Problem 1](./Problem1.md)
 
-* [Problem 2](./Problem2.md)
+* [Problem 2](./Problem2.md)
+
+* [Problem 3](./Problem3.md)
+
+* [Problem 4](./Problem4.md)