comment - heterogeneous boolean equality

lukaszcz · lukaszcz · commit b90edd20d314 · 2025-09-17T18:44:14.000+02:00
diff --git a/Prelude/HBeq.lean b/Prelude/HBeq.lean
@@ -1,6 +1,7 @@
 class HBEq (α β : Type u) where
   hbeq : α → β → Bool
 
+/-- Heterogeneous boolean equality. -/
 infix:50 " ≍? " => HBEq.hbeq
 
 instance BEq.instHBEq (α : Type u) [BEq α] : HBEq α α where
