diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index e18dac58c9..10113a4b00 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -77,7 +77,7 @@ macro_rules
     for (c₁, c₂) in cs₁.zip cs₂ |>.reverse do
       body ← `($c₁ = $c₂ → $body)
     let hint : Ident ← `(hint)
-    `($[$doc?:docComment]? @[$kind unification_hint] def $(n.getD hint) $bs* : Sort _ := $body)
+    `($[$doc?:docComment]? @[$kind unification_hint, expose] def $(n.getD hint) $bs* : Sort _ := $body)
 end Lean
 
 open Lean