From f3119f51d94359807a551a14cd742467f0bdc4ab Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 21 Apr 2024 21:15:37 +0900
Subject: [PATCH] format code: `deriving` and `where` in def

---
 Src/Problem11.lean |  2 +-
 Src/Problem12.lean |  2 +-
 Src/Problem13.lean |  5 +++--
 Src/Problem15.lean |  3 ++-
 Src/Problem16.lean | 15 ++++++++-------
 Src/Problem22.lean |  3 ++-
 Src/Problem24.lean |  3 ++-
 Src/Problem35.lean |  3 ++-
 Src/Problem8.lean  |  3 ++-
 9 files changed, 23 insertions(+), 16 deletions(-)

diff --git a/Src/Problem11.lean b/Src/Problem11.lean
index d78620d..9bc98d7 100644
--- a/Src/Problem11.lean
+++ b/Src/Problem11.lean
@@ -9,7 +9,7 @@ variable {α : Type} [BEq α]
 inductive Data (α : Type) where
   | multiple : Nat → α → Data α
   | single : α → Data α
-  deriving Repr
+deriving Repr
 
 open Data
 
diff --git a/Src/Problem12.lean b/Src/Problem12.lean
index 85d0672..b5b083a 100644
--- a/Src/Problem12.lean
+++ b/Src/Problem12.lean
@@ -9,7 +9,7 @@ variable {α : Type} [BEq α]
 inductive Data (α : Type) where
   | multiple : Nat → α → Data α
   | single : α → Data α
-  deriving Repr
+deriving Repr
 
 open Data
 
diff --git a/Src/Problem13.lean b/Src/Problem13.lean
index fd31438..c4b9df1 100644
--- a/Src/Problem13.lean
+++ b/Src/Problem13.lean
@@ -9,7 +9,7 @@ variable {α : Type} [BEq α] [Inhabited α]
 inductive Data (α : Type) where
   | multiple : Nat → α → Data α
   | single : α → Data α
-  deriving Repr
+deriving Repr
 
 open Data
 
@@ -20,7 +20,8 @@ def encodeDirect (l : List α) : List (Data α) :=
       single a
     else
       multiple n a
-  where counting : List α → List (Nat × α)
+where
+  counting : List α → List (Nat × α)
     | [] => []
     | [a] => [(1, a)]
     | a :: b :: t =>
diff --git a/Src/Problem15.lean b/Src/Problem15.lean
index 9130deb..eb86fe5 100644
--- a/Src/Problem15.lean
+++ b/Src/Problem15.lean
@@ -10,7 +10,8 @@ def repli (l : List α) (n : Nat) : List α :=
   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 => []
     | m + 1 => x :: solorepl x m
diff --git a/Src/Problem16.lean b/Src/Problem16.lean
index c69a8ed..961109d 100644
--- a/Src/Problem16.lean
+++ b/Src/Problem16.lean
@@ -7,13 +7,14 @@ variable {α : Type}
 def dropEvery (l : List α) (n : Nat) : List α :=
   -- sorry
   helper l n 1
-  where helper : List α → Nat → Nat → List α
-    | [], _, _ => []
-    | x :: xs, n, m =>
-      if m % n = 0 then
-        helper xs n (m + 1)
-      else
-        x :: helper xs n (m + 1)
+where
+  helper : List α → Nat → Nat → List α
+  | [], _, _ => []
+  | x :: xs, n, m =>
+    if m % n = 0 then
+      helper xs n (m + 1)
+    else
+      x :: helper xs n (m + 1)
   -- sorry
 
 -- The following codes are for test and you should not edit these.
diff --git a/Src/Problem22.lean b/Src/Problem22.lean
index 6779970..d7114c0 100644
--- a/Src/Problem22.lean
+++ b/Src/Problem22.lean
@@ -6,7 +6,8 @@
 def range (m n : Int) : List Int :=
   -- sorry
   generate m (n - m + 1).toNat
-  where generate (start : Int) (length : Nat) : List Int :=
+where
+  generate (start : Int) (length : Nat) : List Int :=
     match length with
     | 0 => []
     | l + 1 => generate start l ++ [start + l]
diff --git a/Src/Problem24.lean b/Src/Problem24.lean
index 7c3c2c5..7b86edc 100644
--- a/Src/Problem24.lean
+++ b/Src/Problem24.lean
@@ -32,7 +32,8 @@ def diffSelect (count range : Nat) : IO (List Nat) := do
       result := e :: result
 
   return result
-  where extractOne (univ : List Nat) : IO (Option Nat × List Nat) := do
+where
+  extractOne (univ : List Nat) : IO (Option Nat × List Nat) := do
     if univ == [] then
       return (none, [])
 
diff --git a/Src/Problem35.lean b/Src/Problem35.lean
index 658eeec..be42378 100644
--- a/Src/Problem35.lean
+++ b/Src/Problem35.lean
@@ -8,7 +8,8 @@ Construct a flat list containing the prime factors in ascending order.
 def primeFactors (n : Nat) : List Nat :=
   -- sorry
   loop n 2 [] |>.reverse
-  where loop (tgt candidate : Nat) (acc : List Nat) : List Nat :=
+where
+  loop (tgt candidate : Nat) (acc : List Nat) : List Nat :=
     if tgt ≤ 1 || candidate > tgt then
       acc
     else if tgt % candidate = 0 then
diff --git a/Src/Problem8.lean b/Src/Problem8.lean
index 9f73506..3ee4808 100644
--- a/Src/Problem8.lean
+++ b/Src/Problem8.lean
@@ -9,7 +9,8 @@ def compress (l : List α) : List α :=
   match l with
   | [] => []
   | a :: b => a :: comp' b a
-  where comp' (ls : List α) (x : α) : List α :=
+where
+  comp' (ls : List α) (x : α) : List α :=
     match ls with
     | [] => []
     | a' :: l' =>