From 5af6dad9d74f2f0d1733c21535e106644ba5c64c Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Mon, 17 Jun 2024 01:02:33 +0900
Subject: [PATCH] add Problem 28A

---
 Src/Problem28.lean | 34 ++++++++++++++++++++++++++++++++++
 md/SUMMARY.md      |  1 +
 2 files changed, 35 insertions(+)
 create mode 100644 Src/Problem28.lean

diff --git a/Src/Problem28.lean b/Src/Problem28.lean
new file mode 100644
index 0000000..761850a
--- /dev/null
+++ b/Src/Problem28.lean
@@ -0,0 +1,34 @@
+/- # Problem 28A
+(Intermediate 🌟🌟) Sorting a list of lists according to length of sublists.
+-/
+variable {α : Type}
+
+def orderedInsert (a : α) (ord : α → Nat) : List α → List α
+  | [] => [a]
+  | b :: l =>
+    if ord a ≤ ord b then a :: b :: l
+    else b :: orderedInsert a ord l
+
+/-- insertion sort -/
+def insertionSort (ord : α → Nat) : List α → List α
+  | [] => []
+  | b :: l => orderedInsert b ord <| insertionSort ord l
+
+#guard insertionSort (fun x => x) [3, 1, 4, 1, 5, 9, 2, 6, 5, 3, 5]
+  = [1, 1, 2, 3, 3, 4, 5, 5, 5, 6, 9]
+
+-- You can use this!
+#check insertionSort
+
+def lsort (l : List (List α)) : List (List α) :=
+  -- sorry
+  insertionSort (fun l => l.length) l
+  -- sorry
+
+-- The following codes are for test and you should not edit these.
+
+#guard lsort [["a", "b", "c"], ["a", "b"], ["a"]]
+  = [["a"], ["a", "b"], ["a", "b", "c"]]
+
+#guard lsort [[3, 1, 4], [1, 5, 9, 2], [6, 5, 3, 5], [1]]
+  = [[1], [3, 1, 4], [1, 5, 9, 2], [6, 5, 3, 5]]
diff --git a/md/SUMMARY.md b/md/SUMMARY.md
index 969eb4c..0e865bb 100644
--- a/md/SUMMARY.md
+++ b/md/SUMMARY.md
@@ -37,6 +37,7 @@
 * [25: Random permutation](./build/Problem25.md)
 * [26: Generate combinations](./build/Problem26.md)
 * [27: Group into disjoint subsets](./build/Problem27.md)
+* [28A: Sorting a list of lists](./build/Problem28.md)
 
 # 31-41: Arithmetic