update problem name

lean-ja · Oct 26, 2024 · 893e9cc · 893e9cc
1 parent 5450c08
commit 893e9cc
Show file tree

Hide file tree

Showing 11 changed files with 64 additions and 64 deletions.
diff --git a/Src/Problem1.lean → Src/Problem01.lean b/Src/Problem1.lean → Src/Problem01.lean
diff --git a/Src/Problem2.lean → Src/Problem02.lean b/Src/Problem2.lean → Src/Problem02.lean
diff --git a/Src/Problem3.lean → Src/Problem03.lean b/Src/Problem3.lean → Src/Problem03.lean
diff --git a/Src/Problem4.lean → Src/Problem04.lean b/Src/Problem4.lean → Src/Problem04.lean
diff --git a/Src/Problem5.lean → Src/Problem05.lean b/Src/Problem5.lean → Src/Problem05.lean
diff --git a/Src/Problem6.lean → Src/Problem06.lean b/Src/Problem6.lean → Src/Problem06.lean
diff --git a/Src/Problem7.lean → Src/Problem07.lean b/Src/Problem7.lean → 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 → Src/Problem08.lean b/Src/Problem8.lean → Src/Problem08.lean
diff --git a/Src/Problem9.lean → Src/Problem09.lean b/Src/Problem9.lean → Src/Problem09.lean
diff --git 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
@@ -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