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