From 39f253277233b27ad12fa33912fc2093451ff0b3 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Sat, 15 Feb 2025 01:31:14 +0000 Subject: [PATCH] chore(Logic): give implicit argument an accessible name --- Batteries/Logic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Batteries/Logic.lean b/Batteries/Logic.lean index 0be01f3b28..363b0fc94f 100644 --- 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