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..ba0f195 --- /dev/null +++ b/Src/Problem14.lean @@ -0,0 +1,22 @@ +/- + # 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..f13b1a9 --- /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 => [] + | 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] 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)