From 71ddf227d2effc7725bf20e655a806a461e26cfe Mon Sep 17 00:00:00 2001
From: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Date: Thu, 9 Oct 2025 12:10:23 +0200
Subject: [PATCH] doc: add a recommended spelling for `HEq` (#10717)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds a recommended spelling for heterogenous equality (`HEq`,
`≍`).
---
 src/Init/Notation.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 1d4ded4699..504b1ede61 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -402,6 +402,7 @@ recommended_spelling "ge" for "≥" in [GE.ge, «term_≥_»]
 recommended_spelling "ge" for ">=" in [GE.ge, «term_>=_»]
 recommended_spelling "eq" for "=" in [Eq, «term_=_»]
 recommended_spelling "beq" for "==" in [BEq.beq, «term_==_»]
+recommended_spelling "heq" for "≍" in [HEq, «term_≍_»]
 
 @[inherit_doc] infixr:35 " /\\ " => And
 @[inherit_doc] infixr:35 " ∧ "   => And