format code

Src/Problem14.lean

@@ -14,8 +14,9 @@ def dupli (l : List α) : List α :=
 
 -- The following code is a test case and you should not change it.
 
-example : dupli [1,2,3] = [1,1,2,2,3,3] := by rfl
+example : dupli [1, 2, 3] = [1, 1, 2, 2, 3, 3] := by rfl
 
 example : dupli ([] : List α) = [] := by rfl
 
-example : dupli ['a','b','c','c','d'] = ['a','a','b','b','c','c','c','c','d','d'] := by rfl
+example : dupli ['a', 'b', 'c', 'c', 'd']
+  = ['a', 'a', 'b', 'b', 'c', 'c', 'c', 'c', 'd', 'd'] := by rfl

Src/Problem15.lean

@@ -5,25 +5,25 @@
 
 variable {α : Type}
 
-def repli (l : List α)(n : Nat) : List α :=
+def repli (l : List α) (n : Nat) : List α :=
   -- sorry
   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 => []
-    | Nat.succ m => x :: solorepl x m
+    | m + 1 => x :: solorepl x m
   -- sorry
 
 -- The following code is a test case and you should not change it.
 
-example : repli [1,2,3] 3 = [1,1,1,2,2,2,3,3,3] := by rfl
+example : repli [1, 2, 3] 3 = [1, 1, 1, 2, 2, 2, 3, 3, 3] := by rfl
 
-example : repli [1,2,3] 2 = [1,1,2,2,3,3] := by rfl
+example : repli [1, 2, 3] 2 = [1, 1, 2, 2, 3, 3] := by rfl
 
-example : repli [1,2,3] 1 = [1,2,3] := by rfl
+example : repli [1, 2, 3] 1 = [1, 2, 3] := by rfl
 
-example : repli [1,2,3] 0 = [] := by rfl
+example : repli [1, 2, 3] 0 = [] := by rfl
 
 example : repli ([] : List α) 255 = [] := by rfl