fix: unused variables (#802)

leanprover-community · May 17, 2024 · cff1ec6 · cff1ec6
1 parent 914ad4f
commit cff1ec6
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/Batteries/Data/BinomialHeap/Basic.lean b/Batteries/Data/BinomialHeap/Basic.lean
@@ -394,10 +394,10 @@ theorem Heap.WF.merge' (h₁ : s₁.WF le n) (h₂ : s₂.WF le n) :
     · let ⟨ih₁, ih₂⟩ := merge' (s₁ := .cons ..)
         ⟨Nat.le_succ_of_le hr₁, this, ht₁.of_rankGT hl₁⟩
         (ht₂.of_le (Nat.le_succ_of_le hr₁))
-      exact ⟨ih₁, fun _ => ih₂ ⟨fun _ => ht₂.rankGT.of_le hr₁, fun h => Nat.lt_succ_of_le hr₁⟩⟩
+      exact ⟨ih₁, fun _ => ih₂ ⟨fun _ => ht₂.rankGT.of_le hr₁, fun _ => Nat.lt_succ_of_le hr₁⟩⟩
     · let ⟨ih₁, ih₂⟩ := merge' (s₂ := .cons ..) (ht₁.of_le (Nat.le_succ_of_le hr₁))
         ⟨Nat.le_succ_of_le hr₁, this, ht₂.of_rankGT hl₂⟩
-      exact ⟨ih₁, fun _ => ih₂ ⟨fun h => Nat.lt_succ_of_le hr₁, fun _ => ht₁.rankGT.of_le hr₁⟩⟩
+      exact ⟨ih₁, fun _ => ih₂ ⟨fun _ => Nat.lt_succ_of_le hr₁, fun _ => ht₁.rankGT.of_le hr₁⟩⟩
     · let ⟨ih₁, ih₂⟩ := merge' ht₁ ht₂
       exact ⟨⟨Nat.le_succ_of_le hr₁, this, ih₁.of_rankGT (ih₂ (iff_of_false hl₁ hl₂))⟩,
         fun _ => Nat.lt_succ_of_le hr₁⟩

diff --git a/Batteries/Data/PairingHeap.lean b/Batteries/Data/PairingHeap.lean
@@ -246,8 +246,8 @@ theorem Heap.WF.merge (h₁ : s₁.WF le) (h₂ : s₂.WF le) :
 theorem Heap.WF.combine (h : s.NodeWF le a) : (combine le s).WF le :=
   match s with
   | .nil => nil
-  | .node b c .nil => node h.2.1
-  | .node b₁ c₁ (.node b₂ c₂ s) => merge (merge_node h.2.1 h.2.2.2.1) (combine h.2.2.2.2)
+  | .node _b _c .nil => node h.2.1
+  | .node _b₁ _c₁ (.node _b₂ _c₂ _s) => merge (merge_node h.2.1 h.2.2.2.1) (combine h.2.2.2.2)
 
 theorem Heap.WF.deleteMin {s : Heap α} (h : s.WF le)
     (eq : s.deleteMin le = some (a, s')) : s'.WF le := by

diff --git a/Batteries/Data/RBMap/Alter.lean b/Batteries/Data/RBMap/Alter.lean
@@ -100,8 +100,8 @@ protected theorem Balanced.ins {path : Path α}
     | .balanced .nil => exact ih (.balanced (.red hl .nil))
     | .balanced (.red ha hb) => exact ih (.redred rfl hl (.red ha hb))
     | .balanced (.black ha hb) => exact ih (.balanced (.red hl (.black ha hb)))
-  | blackL hr hp ih => exact have ⟨c, h⟩ := ht.balance1 hr; ih (.balanced h)
-  | blackR hl hp ih => exact have ⟨c, h⟩ := ht.balance2 hl; ih (.balanced h)
+  | blackL hr _hp ih => exact have ⟨c, h⟩ := ht.balance1 hr; ih (.balanced h)
+  | blackR hl _hp ih => exact have ⟨c, h⟩ := ht.balance2 hl; ih (.balanced h)
 
 protected theorem Balanced.insertNew {path : Path α} (H : path.Balanced c n black 0) :
     ∃ n, (path.insertNew v).Balanced black n := H.ins (.balanced (.red .nil .nil))