From d07ec9a19fbea59f2a9b0ef34e360fdd28ae9935 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 5 Aug 2025 17:59:49 +0200
Subject: [PATCH] chore: show `@[expose]` attribute in `#print` (#9722)

---
 src/Lean/Elab/Print.lean           |  4 ++++
 tests/lean/run/derivingRepr.lean   |  2 +-
 tests/pkg/module/Module/Basic.lean | 27 ++++++++++++++++++++++++++-
 3 files changed, 31 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index 66ac83f913..913e72473d 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -34,6 +34,10 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
   | ReducibilityStatus.reducible =>     attrs := attrs.push m!"reducible"
   | ReducibilityStatus.semireducible => pure ()
 
+  let env ← getEnv
+  if env.header.isModule && (env.setExporting true |>.find? id |>.any (·.isDefinition)) then
+    attrs := attrs.push m!"expose"
+
   if defeqAttr.hasTag (← getEnv) id then
     attrs := attrs.push m!"defeq"
 
diff --git a/tests/lean/run/derivingRepr.lean b/tests/lean/run/derivingRepr.lean
index 392399e175..eeb971d90c 100644
--- a/tests/lean/run/derivingRepr.lean
+++ b/tests/lean/run/derivingRepr.lean
@@ -152,7 +152,7 @@ public structure Public where
 deriving Repr
 
 /--
-info: def instReprPublic : Repr Public :=
+info: @[expose] def instReprPublic : Repr Public :=
 { reprPrec := reprPublic✝ }
 -/
 #guard_msgs in
diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean
index 6c5db2c64d..486b358e61 100644
--- a/tests/pkg/module/Module/Basic.lean
+++ b/tests/pkg/module/Module/Basic.lean
@@ -6,9 +6,34 @@ public axiom testSorry : α
 
 /-- A definition (not exposed). -/
 public def f := 1
-/-- An definition (exposed) -/
+
+/--
+info: def f : Nat :=
+1
+-/
+#guard_msgs in
+#print f
+
+/-- A definition (exposed) -/
 @[expose] public def fexp := 1
 
+/--
+info: @[expose] def fexp : Nat :=
+1
+-/
+#guard_msgs in
+#print fexp
+
+/-- An abbrev (auto-exposed). -/
+public abbrev fabbrev := 1
+
+/--
+info: @[reducible, expose] def fabbrev : Nat :=
+1
+-/
+#guard_msgs in
+#print fabbrev
+
 #guard_msgs(drop warning) in
 /-- A theorem. -/
 public theorem t : f = 1 := testSorry