chore(Logic): give implicit argument an accessible name (leanprover-c…

…ommunity#1136)
fgdorais · Feb 15, 2025 · 80520e5 · 80520e5
1 parent 327d6ed
commit 80520e5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Batteries/Logic.lean b/Batteries/Logic.lean
@@ -26,7 +26,7 @@ end Classical
 
 /-! ## equality -/
 
-theorem heq_iff_eq : HEq a b ↔ a = b := ⟨eq_of_heq, heq_of_eq⟩
+theorem heq_iff_eq {a b : α} : HEq a b ↔ a = b := ⟨eq_of_heq, heq_of_eq⟩
 
 @[simp] theorem eq_rec_constant {α : Sort _} {a a' : α} {β : Sort _} (y : β) (h : a = a') :
     (@Eq.rec α a (fun _ _ => β) y a' h) = y := by cases h; rfl