From 671057eecf8d4b9af64ade4650ade3ebe6df9036 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 25 Jul 2025 11:05:31 +0200 Subject: [PATCH] fix: `unif_hint` under the module system (#9530) --- src/Init/NotationExtra.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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