From 6862b90c2fe6601732908ebc303aeb09e543cb52 Mon Sep 17 00:00:00 2001
From: Csharpython <ykt8910@gmail.com>
Date: Mon, 18 Mar 2024 20:04:01 +0900
Subject: [PATCH 1/2] Solve Q14,Q15

---
 Src.lean           |  2 ++
 Src/Problem14.lean | 21 +++++++++++++++++++++
 Src/Problem15.lean | 29 +++++++++++++++++++++++++++++
 md/SUMMARY.md      |  5 +++++
 4 files changed, 57 insertions(+)
 create mode 100644 Src/Problem14.lean
 create mode 100644 Src/Problem15.lean

diff --git a/Src.lean b/Src.lean
index 52f6cb3..29fa8ec 100644
--- a/Src.lean
+++ b/Src.lean
@@ -1,5 +1,7 @@
 import Src.Problem1
 import Src.Problem10
+import Src.Problem14
+import Src.Problem15
 import Src.Problem2
 import Src.Problem3
 import Src.Problem31
diff --git a/Src/Problem14.lean b/Src/Problem14.lean
new file mode 100644
index 0000000..e7406f0
--- /dev/null
+++ b/Src/Problem14.lean
@@ -0,0 +1,21 @@
+/-
+  # Problem 14
+  Duplicate the elements of a list.
+-/
+
+variable {α : Type}
+
+def dupli (l : List α) : List α :=
+  -- sorry
+  match l with
+  | [] => []
+  | a :: b => a :: a :: dupli b
+  -- sorry
+
+-- The following code is a test case and you should not change it.
+
+example : dupli [1,2,3] = [1,1,2,2,3,3] := by rfl
+
+example : dupli ([] : List α) = [] := by rfl
+
+example : dupli ['a','b','c','c','d'] = ['a','a','b','b','c','c','c','c','d','d'] := by rfl
diff --git a/Src/Problem15.lean b/Src/Problem15.lean
new file mode 100644
index 0000000..3f6d0b2
--- /dev/null
+++ b/Src/Problem15.lean
@@ -0,0 +1,29 @@
+/-
+  # Problem 15
+  Replicate the elements of a list a given number of times.
+-/
+
+variable {α : Type}
+
+def repli (l : List α)(n : Nat) : List α :=
+  -- sorry
+  match l with
+  | [] => []
+  | a :: b => (solorepl a n) ++ repli b n
+  where solorepl (x : α)(n : Nat) : List α :=
+    match n with
+    | 0 => []
+    | Nat.succ m => x :: solorepl x m
+  -- sorry
+
+-- The following code is a test case and you should not change it.
+
+example : repli [1,2,3] 3 = [1,1,1,2,2,2,3,3,3] := by rfl
+
+example : repli [1,2,3] 2 = [1,1,2,2,3,3] := by rfl
+
+example : repli [1,2,3] 1 = [1,2,3] := by rfl
+
+example : repli [1,2,3] 0 = [] := by rfl
+
+example : repli ([] : List α) 255 = [] := by rfl
diff --git a/md/SUMMARY.md b/md/SUMMARY.md
index 0844507..7fc550f 100644
--- a/md/SUMMARY.md
+++ b/md/SUMMARY.md
@@ -15,6 +15,11 @@
 * [9: Pack consecutive duplicates](./build/Problem9.md)
 * [10: Run-length encoding](./build/Problem10.md)
 
+# 11-20: Lists, continued
+
+* [14: Duplicate elements](./build/Problem14.md)
+* [15: Replicate elements K times](./build/Problem15.md)
+
 # 31-40: Arithmetic
 
 * [31: Prime number detection](./build/Problem31.md)

From 331d99efc51bc0885270606ff9214f1a4603b732 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 18 Mar 2024 20:53:16 +0900
Subject: [PATCH 2/2] format code

---
 Src/Problem14.lean |  5 +++--
 Src/Problem15.lean | 14 +++++++-------
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/Src/Problem14.lean b/Src/Problem14.lean
index e7406f0..ba0f195 100644
--- a/Src/Problem14.lean
+++ b/Src/Problem14.lean
@@ -14,8 +14,9 @@ def dupli (l : List α) : List α :=
 
 -- The following code is a test case and you should not change it.
 
-example : dupli [1,2,3] = [1,1,2,2,3,3] := by rfl
+example : dupli [1, 2, 3] = [1, 1, 2, 2, 3, 3] := by rfl
 
 example : dupli ([] : List α) = [] := by rfl
 
-example : dupli ['a','b','c','c','d'] = ['a','a','b','b','c','c','c','c','d','d'] := by rfl
+example : dupli ['a', 'b', 'c', 'c', 'd']
+  = ['a', 'a', 'b', 'b', 'c', 'c', 'c', 'c', 'd', 'd'] := by rfl
diff --git a/Src/Problem15.lean b/Src/Problem15.lean
index 3f6d0b2..f13b1a9 100644
--- a/Src/Problem15.lean
+++ b/Src/Problem15.lean
@@ -5,25 +5,25 @@
 
 variable {α : Type}
 
-def repli (l : List α)(n : Nat) : List α :=
+def repli (l : List α) (n : Nat) : List α :=
   -- sorry
   match l with
   | [] => []
   | a :: b => (solorepl a n) ++ repli b n
-  where solorepl (x : α)(n : Nat) : List α :=
+  where solorepl (x : α) (n : Nat) : List α :=
     match n with
     | 0 => []
-    | Nat.succ m => x :: solorepl x m
+    | m + 1 => x :: solorepl x m
   -- sorry
 
 -- The following code is a test case and you should not change it.
 
-example : repli [1,2,3] 3 = [1,1,1,2,2,2,3,3,3] := by rfl
+example : repli [1, 2, 3] 3 = [1, 1, 1, 2, 2, 2, 3, 3, 3] := by rfl
 
-example : repli [1,2,3] 2 = [1,1,2,2,3,3] := by rfl
+example : repli [1, 2, 3] 2 = [1, 1, 2, 2, 3, 3] := by rfl
 
-example : repli [1,2,3] 1 = [1,2,3] := by rfl
+example : repli [1, 2, 3] 1 = [1, 2, 3] := by rfl
 
-example : repli [1,2,3] 0 = [] := by rfl
+example : repli [1, 2, 3] 0 = [] := by rfl
 
 example : repli ([] : List α) 255 = [] := by rfl