From 743810b77af561c11f0d024372c0eec882bc6d90 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Nov 2021 07:46:10 -0800
Subject: [PATCH] feat: use `binrel_no_prop%` to define `==` notation

fixes #764
---
 src/Init/Notation.lean  | 2 +-
 tests/lean/run/764.lean | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/764.lean

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 8c425b3c8f..46fa8095e3 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -113,7 +113,7 @@ macro_rules | `($x > $y)  => `(binrel% GT.gt $x $y)
 macro_rules | `($x >= $y) => `(binrel% GE.ge $x $y)
 macro_rules | `($x ≥ $y)  => `(binrel% GE.ge $x $y)
 macro_rules | `($x = $y)  => `(binrel% Eq $x $y)
-macro_rules | `($x == $y) => `(binrel% BEq.beq $x $y)
+macro_rules | `($x == $y) => `(binrel_no_prop% BEq.beq $x $y)
 
 infixr:35 " /\\ " => And
 infixr:35 " ∧ "   => And
diff --git a/tests/lean/run/764.lean b/tests/lean/run/764.lean
new file mode 100644
index 0000000000..6f4d0c5162
--- /dev/null
+++ b/tests/lean/run/764.lean
@@ -0,0 +1,6 @@
+#eval (5 > 2) == true
+#eval (2 > 5) == true
+
+variable (b : Bool)
+
+#check (5 > 2) == b