diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index aa4537ffb5..19a60c9f67 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -128,7 +128,7 @@ infixl:30 " || " => or
 notation:max "!" b:40 => not b
 
 infixr:67 " :: " => List.cons
-infixr:20 " <|> " => HOrElse.hOrElse
+syntax:20 term:21 " <|> " term:20 : term
 infixr:60  " >> "  => HAndThen.hAndThen
 infixl:55  " >>= " => Bind.bind
 infixl:60  " <*> " => Seq.seq
diff --git a/tests/lean/eagerCoeExpansion.lean.expected.out b/tests/lean/eagerCoeExpansion.lean.expected.out
index 8bd74e2eeb..ab4180aa42 100644
--- a/tests/lean/eagerCoeExpansion.lean.expected.out
+++ b/tests/lean/eagerCoeExpansion.lean.expected.out
@@ -22,4 +22,4 @@ fun (a : Nat) =>
         (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
       true)
 def s : Option Nat :=
-ConstantFunction.f myFun 3 <|> ConstantFunction.f myFun 4
+HOrElse.hOrElse (ConstantFunction.f myFun 3) fun x => ConstantFunction.f myFun 4