fix: unused arguments (#277)

Author: gebner

Mathlib/Data/BinaryHeap.lean

@@ -51,7 +51,7 @@ def mkHeap (lt : α → α → Bool) (a : Array α) : {a' : Array α // a'.size
     ⟨a₂, h₂.trans a'.2⟩
   loop (a.size / 2) a (Nat.div_le_self ..)
 
-@[simp] theorem size_mkHeap (lt : α → α → Bool) (a : Array α) (i : Fin a.size) :
+@[simp] theorem size_mkHeap (lt : α → α → Bool) (a : Array α) :
   (mkHeap lt a).1.size = a.size := (mkHeap lt a).2
 
 /-- Core operation for binary heaps, expressed directly on arrays.

Mathlib/Data/List/Basic.lean

@@ -649,7 +649,7 @@ theorem get_of_eq {L L' : List α} (h : L = L') (i : Fin  L.length) :
   cases n
   subst hn0; rfl
 
-theorem get_zero [Inhabited α] {L : List α} (h : 0 < L.length) : L.get ⟨0, h⟩ = L.head? := by
+theorem get_zero {L : List α} (h : 0 < L.length) : L.get ⟨0, h⟩ = L.head? := by
   cases L; {cases h}; simp
 
 theorem get_append : ∀ {l₁ l₂ : List α} (n : ℕ) (h : n < l₁.length),
@@ -1241,12 +1241,12 @@ repeat' a (n - length l) ++ l
 theorem leftpad_length (n : ℕ) (a : α) (l : List α) : (leftpad n a l).length = max n l.length :=
 by simp only [leftpad, length_append, length_repeat', Nat.sub_add_eq_max]
 
-theorem leftpad_prefix [DecidableEq α] (n : ℕ) (a : α) (l : List α) : isPrefix (repeat' a (n - length l)) (leftpad n a l) :=
+theorem leftpad_prefix (n : ℕ) (a : α) (l : List α) : isPrefix (repeat' a (n - length l)) (leftpad n a l) :=
 by
   simp only [isPrefix, leftpad]
   exact Exists.intro l rfl
 
-theorem leftpad_suffix [DecidableEq α] (n : ℕ) (a : α) (l : List α) : isSuffix l (leftpad n a l) :=
+theorem leftpad_suffix (n : ℕ) (a : α) (l : List α) : isSuffix l (leftpad n a l) :=
 by
   simp only [isSuffix, leftpad]
   exact Exists.intro (repeat' a (n - length l)) rfl

Mathlib/Data/UnionFind.lean

@@ -39,7 +39,7 @@ def setParent {n} (m : UFModel n) (x y : Fin n) (h : m.rank x < m.rank y) : UFMo
     · exact m.rank_lt i
 
 def setParentBump {n} (m : UFModel n) (x y : Fin n)
-  (ne : x.1 ≠ y) (H : m.rank x ≤ m.rank y) (hroot : (m.parent y).1 = y) : UFModel n where
+    (H : m.rank x ≤ m.rank y) (hroot : (m.parent y).1 = y) : UFModel n where
   parent i := if x.1 = i then y else m.parent i
   rank i := if y.1 = i ∧ m.rank x = m.rank y then m.rank y + 1 else m.rank i
   rank_lt i := by
@@ -273,7 +273,7 @@ def link (self : UnionFind α) (x y : Fin self.size)
   case b =>
     let ⟨m, hm⟩ := self.model'; let n := self.size
     simp [hm.rank_eq] at h; simp [hm.parent_eq'] at yroot
-    refine ⟨_, m.setParentBump x y ne h yroot, ?_⟩
+    refine ⟨_, m.setParentBump x y h yroot, ?_⟩
     let parent (i : Fin n) := (if x.1 = i then y else m.parent i).1
     have : UFModel.Agrees arr₁ (·.parent) parent :=
       hm.1.set (fun i h => by simp; rw [if_neg h.symm]) (fun h => by simp)

Mathlib/Tactic/Core.lean

@@ -55,8 +55,9 @@ def toPreDefinition (nm newNm : Name) (newType newValue : Expr) (newDoc : Option
     type := newType
     value := newValue }
   return predef
+
 /-- Make `nm` protected. -/
-def setProtected {m : Type → Type} [Monad m] [MonadEnv m] (nm : Name) : m Unit := do
+def setProtected {m : Type → Type} [MonadEnv m] (nm : Name) : m Unit :=
   modifyEnv (addProtected · nm)
 
 namespace Parser.Tactic

Mathlib/Testing/SlimCheck/Testable.lean

@@ -404,14 +404,14 @@ section IO
 open TestResult
 
 /-- Execute `cmd` and repeat every time the result is `gave_up` (at most `n` times). -/
-def retry (cmd : Rand (TestResult p)) (cfg : Configuration) : Nat → Rand (TestResult p)
+def retry (cmd : Rand (TestResult p)) : Nat → Rand (TestResult p)
 | 0 => pure $ TestResult.gaveUp 1
 | n+1 => do
   let r ← cmd
   match r with
   | success hp => pure $ success hp
   | TestResult.failure h xs n => pure $ failure h xs n
-  | gaveUp _ => retry cmd cfg n
+  | gaveUp _ => retry cmd n
 
 /-- Count the number of times the test procedure gave up. -/
 def giveUp (x : Nat) : TestResult p → TestResult p
@@ -428,7 +428,7 @@ def Testable.runSuiteAux (p : Prop) [Testable p] (cfg : Configuration) : TestRes
   if cfg.traceSuccesses then
     slimTrace s!"New sample"
     slimTrace s!"Retrying up to {cfg.numRetries} times until guards hold"
-  let x ← retry (ReaderT.run (Testable.runProp p cfg true) ⟨size⟩) cfg cfg.numRetries
+  let x ← retry (ReaderT.run (Testable.runProp p cfg true) ⟨size⟩) cfg.numRetries
   match x with
   | (success (PSum.inl ())) => runSuiteAux p cfg r n
   | (gaveUp g) => runSuiteAux p cfg (giveUp g r) n