chore: show @[expose] attribute in #print (#9722)

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"
 

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

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