From 893e9cc321a7a0e2bad8df73ca382763d404d253 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 26 Oct 2024 09:56:01 +0900 Subject: [PATCH] update problem name --- Src/{Problem1.lean => Problem01.lean} | 0 Src/{Problem2.lean => Problem02.lean} | 0 Src/{Problem3.lean => Problem03.lean} | 0 Src/{Problem4.lean => Problem04.lean} | 0 Src/{Problem5.lean => Problem05.lean} | 0 Src/{Problem6.lean => Problem06.lean} | 0 Src/{Problem7.lean => Problem07.lean} | 108 +++++++++++++------------- Src/{Problem8.lean => Problem08.lean} | 0 Src/{Problem9.lean => Problem09.lean} | 0 Src/Problem41.lean | 2 +- md/SUMMARY.md | 18 ++--- 11 files changed, 64 insertions(+), 64 deletions(-) rename Src/{Problem1.lean => Problem01.lean} (100%) rename Src/{Problem2.lean => Problem02.lean} (100%) rename Src/{Problem3.lean => Problem03.lean} (100%) rename Src/{Problem4.lean => Problem04.lean} (100%) rename Src/{Problem5.lean => Problem05.lean} (100%) rename Src/{Problem6.lean => Problem06.lean} (100%) rename Src/{Problem7.lean => Problem07.lean} (96%) rename Src/{Problem8.lean => Problem08.lean} (100%) rename Src/{Problem9.lean => Problem09.lean} (100%) diff --git a/Src/Problem1.lean b/Src/Problem01.lean similarity index 100% rename from Src/Problem1.lean rename to Src/Problem01.lean diff --git a/Src/Problem2.lean b/Src/Problem02.lean similarity index 100% rename from Src/Problem2.lean rename to Src/Problem02.lean diff --git a/Src/Problem3.lean b/Src/Problem03.lean similarity index 100% rename from Src/Problem3.lean rename to Src/Problem03.lean diff --git a/Src/Problem4.lean b/Src/Problem04.lean similarity index 100% rename from Src/Problem4.lean rename to Src/Problem04.lean diff --git a/Src/Problem5.lean b/Src/Problem05.lean similarity index 100% rename from Src/Problem5.lean rename to Src/Problem05.lean diff --git a/Src/Problem6.lean b/Src/Problem06.lean similarity index 100% rename from Src/Problem6.lean rename to Src/Problem06.lean diff --git a/Src/Problem7.lean b/Src/Problem07.lean similarity index 96% rename from Src/Problem7.lean rename to Src/Problem07.lean index 7db938c..3428953 100644 --- a/Src/Problem7.lean +++ b/Src/Problem07.lean @@ -1,54 +1,54 @@ -/- -# Problem 7 -(Intermediate 🌟🌟) Flatten a nested list structure. --/ - -variable {α : Type} - --- We have to define a new data type, because lists in Lean are homogeneous. -inductive NestedList (α : Type) where - | elem : α → NestedList α - | list : List (NestedList α) → NestedList α - -/-- convert NestedList to String. -/ -partial def NestedList.toString [ToString α] : NestedList α → String - | NestedList.elem x => ToString.toString x - | NestedList.list xs => "[" ++ String.intercalate ", " (xs.map toString) ++ "]" - -/-- Display `NestedList` in a readable manner when you run `#eval`. -/ -instance [ToString α] : ToString (NestedList (α : Type)) where - toString nl := NestedList.toString nl - -/-- flatten the list structure -/ -def flatten (nl : NestedList α) : List α := - -- sorry - match nl with - | .elem x => [x] - | .list [] => [] - | .list (x :: xs) => flatten x ++ flatten (.list xs) - -- sorry - --- The following codes are for test and you should not edit these. - -open NestedList - -def sample : NestedList Nat := - list [elem 1, list [elem 2, elem 3], elem 4] - -#eval sample - -def empty : NestedList String := list [] - -#eval empty - -example : flatten (.elem 5) = [5] := by - delta flatten - rfl - -example : flatten sample = [1, 2, 3, 4] := by - delta flatten - rfl - -example : flatten (empty) = [] := by - delta flatten - rfl +/- +# Problem 7 +(Intermediate 🌟🌟) Flatten a nested list structure. +-/ + +variable {α : Type} + +-- We have to define a new data type, because lists in Lean are homogeneous. +inductive NestedList (α : Type) where + | elem : α → NestedList α + | list : List (NestedList α) → NestedList α + +/-- convert NestedList to String. -/ +partial def NestedList.toString [ToString α] : NestedList α → String + | NestedList.elem x => ToString.toString x + | NestedList.list xs => "[" ++ String.intercalate ", " (xs.map toString) ++ "]" + +/-- Display `NestedList` in a readable manner when you run `#eval`. -/ +instance [ToString α] : ToString (NestedList (α : Type)) where + toString nl := NestedList.toString nl + +/-- flatten the list structure -/ +def flatten (nl : NestedList α) : List α := + -- sorry + match nl with + | .elem x => [x] + | .list [] => [] + | .list (x :: xs) => flatten x ++ flatten (.list xs) + -- sorry + +-- The following codes are for test and you should not edit these. + +open NestedList + +def sample : NestedList Nat := + list [elem 1, list [elem 2, elem 3], elem 4] + +#eval sample + +def empty : NestedList String := list [] + +#eval empty + +example : flatten (.elem 5) = [5] := by + delta flatten + rfl + +example : flatten sample = [1, 2, 3, 4] := by + delta flatten + rfl + +example : flatten (empty) = [] := by + delta flatten + rfl diff --git a/Src/Problem8.lean b/Src/Problem08.lean similarity index 100% rename from Src/Problem8.lean rename to Src/Problem08.lean diff --git a/Src/Problem9.lean b/Src/Problem09.lean similarity index 100% rename from Src/Problem9.lean rename to Src/Problem09.lean diff --git a/Src/Problem41.lean b/Src/Problem41.lean index 06a13b4..97c0481 100644 --- a/Src/Problem41.lean +++ b/Src/Problem41.lean @@ -1,4 +1,4 @@ -/- # Problem 40 +/- # Problem 41 (Intermediate 🌟🌟) A list of even numbers and their Goldbach compositions in a given range. -/ diff --git a/md/SUMMARY.md b/md/SUMMARY.md index 4d47170..0ac0af0 100644 --- a/md/SUMMARY.md +++ b/md/SUMMARY.md @@ -4,15 +4,15 @@ # 1-10: Lists -* [1: Find the last element](./build/Problem1.md) -* [2: Find the second-last element](./build/Problem2.md) -* [3: Find the K'th element](./build/Problem3.md) -* [4: Find the number of elements](./build/Problem4.md) -* [5: Reverse a list](./build/Problem5.md) -* [6: Detect palindrome](./build/Problem6.md) -* [7: Flatten a nested list](./build/Problem7.md) -* [8: Eliminate consecutive duplicates](./build/Problem8.md) -* [9: Pack consecutive duplicates](./build/Problem9.md) +* [1: Find the last element](./build/Problem01.md) +* [2: Find the second-last element](./build/Problem02.md) +* [3: Find the K'th element](./build/Problem03.md) +* [4: Find the number of elements](./build/Problem04.md) +* [5: Reverse a list](./build/Problem05.md) +* [6: Detect palindrome](./build/Problem06.md) +* [7: Flatten a nested list](./build/Problem07.md) +* [8: Eliminate consecutive duplicates](./build/Problem08.md) +* [9: Pack consecutive duplicates](./build/Problem09.md) * [10: Run-length encoding](./build/Problem10.md) # 11-20: Lists, continued