max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: add a recommended spelling for HEq (#10717)

Browse source 
This PR adds a recommended spelling for heterogenous equality (`HEq`,
`≍`).
This commit is contained in:
Rob23oba 2025-10-09 12:10:23 +02:00 • committed by GitHub
parent dca8d6d188
commit 71ddf227d2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/Notation.lean
View file

@ -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