format code: deriving and where in def

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
 

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
 

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 =>

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

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.

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]

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, [])
 

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

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' =>