diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index bec2fc570f..7e018bddb5 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -76,6 +76,21 @@ infixl:75 " >>> "  => HShiftRight.hShiftRight
 infixr:80 " ^ "  => HPow.hPow
 prefix:100 "-"   => Neg.neg
 prefix:100 "~~~"   => Complement.complement
+/-
+  Remark: the infix commands above ensure a delaborator is generated for each relations.
+  We redefine the macros below to be able to use the auxiliary `binop%` elaboration helper for binary operators.
+  It addresses issue #382. -/
+macro_rules | `($x ||| $y) => `(binop% HOr.hOr $x $y)
+macro_rules | `($x ^^^ $y) => `(binop% HXor.hXor $x $y)
+macro_rules | `($x &&& $y) => `(binop% HAnd.hAnd $x $y)
+macro_rules | `($x + $y)   => `(binop% HAdd.hAdd $x $y)
+macro_rules | `($x - $y)   => `(binop% HSub.hSub $x $y)
+macro_rules | `($x * $y)   => `(binop% HMul.hMul $x $y)
+macro_rules | `($x / $y)   => `(binop% HDiv.hDiv $x $y)
+macro_rules | `($x % $y)   => `(binop% HMod.hMod $x $y)
+macro_rules | `($x <<< $y) => `(binop% HShiftLeft.hShiftLeft $x $y)
+macro_rules | `($x >>> $y) => `(binop% HShiftRight.hShiftRight $x $y)
+macro_rules | `($x ^ $y)   => `(binop% HPow.hPow $x $y)
 
 -- declare ASCII alternatives first so that the latter Unicode unexpander wins
 infix:50 " <= " => LE.le
diff --git a/tests/lean/run/382.lean b/tests/lean/run/382.lean
new file mode 100644
index 0000000000..c0923f8daa
--- /dev/null
+++ b/tests/lean/run/382.lean
@@ -0,0 +1,8 @@
+variable (n k : Nat)
+set_option pp.all true
+#check n+k
+#check (n + k : Int)
+#check (n + 1 : Int)
+#check (2 + n : Int)
+#check (1 + 2 : Int)
+#check (1 + 2 * 3 : UInt32)