feat: add Environment.hasExposedBody helper

src/Lean/Elab/Deriving/Basic.lean

@@ -181,7 +181,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) (isNoncomputable
   let decl ← whnfCore decl
   let .const declName _ := decl.getAppFn
     | throwError "Failed to delta derive instance, expecting a term of the form `C ...` where `C` is a constant, given{indentExpr decl}"
-  let exposed := (← getEnv).setExporting true |>.find? declName |>.any (·.hasValue)
+  let exposed := (← getEnv).hasExposedBody declName
   -- When the definition body is private, the deriving handler will need access to the private scope,
   -- and the instance body will automatically be private as well.
   withExporting (isExporting := exposed) do

src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean

@@ -29,7 +29,7 @@ public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
   mkMapDeclarationExtension (exportEntriesFn := fun env s =>
     let all := s.toArray
     -- Do not export for non-exposed defs at exported/server levels
-    let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray
+    let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray
     { exported, server := exported, «private» := all })
 
 public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name)

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -151,7 +151,7 @@ public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
   mkMapDeclarationExtension (exportEntriesFn := fun env s =>
     let all := s.toArray
     -- Do not export for non-exposed defs at exported/server levels
-    let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray
+    let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray
     { exported, server := exported, «private» := all })
 
 public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat)

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -27,7 +27,7 @@ public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
   mkMapDeclarationExtension (exportEntriesFn := fun env s =>
     let all := s.toArray
     -- Do not export for non-exposed defs at exported/server levels
-    let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray
+    let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray
     { exported, server := exported, «private» := all })
 
 public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms)

src/Lean/Environment.lean

@@ -841,6 +841,22 @@ def find? (env : Environment) (n : Name) (skipRealize := false) : Option Constan
     return c
   env.findAsyncCore? n (skipRealize := skipRealize) |>.map (·.toConstantInfo)
 
+/-- Returns `true` iff `n` resolves, in `env`'s exported view, to a `def` with a value.
+
+Concretely this checks whether downstream modules can see a reducible body for `n`
+(an exposed definition or an `abbrev`). Returns `false` for theorems and opaque
+declarations (this uses `hasValue` with `allowOpaque := false`), axioms, inductives,
+constructors, recursors, declarations not in the environment, and `def`s whose body
+is sealed by the module system.
+
+Outside the module system, `setExporting true` is a no-op, so this collapses to
+"does `n` resolve to a `def` in the current environment?". Callers that instead
+want to *bypass* the body-exposed check entirely outside modules (e.g. for name-
+privacy decisions, where there is no sealing boundary anyway) should write that
+policy explicitly: `!env.header.isModule || env.hasExposedBody n`. -/
+def hasExposedBody (env : Environment) (n : Name) : Bool :=
+  env.setExporting true |>.find? n |>.any (·.hasValue)
+
 /--
 Allows `realizeConst` calls for the given declaration in all derived environment branches.
 Realizations will run using the given environment and options to ensure deterministic results. Note

src/Lean/Meta/Constructions/SparseCasesOn.lean

@@ -38,7 +38,7 @@ builtin_initialize sparseCasesOnInfoExt : MapDeclarationExtension SparseCasesOnI
   mkMapDeclarationExtension (exportEntriesFn := fun env s =>
     let all := s.toArray
     -- Do not export for non-exposed defs at exported/server levels
-    let exported := s.filter (fun n _ => (env.setExporting true).find? n |>.any (·.hasValue)) |>.toArray
+    let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray
     { exported, server := exported, «private» := all })
 
 /--

src/Lean/Meta/Eqns.lean

@@ -78,7 +78,7 @@ def declFromEqLikeName (env : Environment) (name : Name) : Option (Name × Strin
   return none
 
 def mkEqLikeNameFor (env : Environment) (declName : Name) (suffix : String) : Name :=
-  let isExposed := !env.header.isModule || ((env.setExporting true).find? declName).elim false (·.hasValue)
+  let isExposed := !env.header.isModule || env.hasExposedBody declName
   let name := .str declName suffix
   let name := if isExposed then name else mkPrivateName env name
   name

src/Lean/Meta/MethodSpecs.lean

@@ -65,7 +65,8 @@ def getMethodSpecsInfo (instName : Name) : MetaM MethodSpecsInfo := do
       unless xs == ys do
         throwError "function `{f}` does not take its arguments in the same order as the instance"
       let implName := f.constName!
-      let isExposed := !(← getEnv).header.isModule || (((← getEnv).setExporting true).find? implName).elim false (·.hasValue)
+      let env ← getEnv
+      let isExposed := !env.header.isModule || env.hasExposedBody implName
       unless isExposed do
         privateSpecs := true
       -- Construct the replacement theorems

tests/elab/hasExposedBody.lean

@@ -0,0 +1,26 @@
+module
+import Lean.Elab.Command
+
+/-!
+# Tests for `Lean.Environment.hasExposedBody`
+
+Confirms the function returns `true` only for `def`s whose body is exposed across
+module boundaries, and `false` for theorems, opaques, axioms, inductives,
+declarations not in the environment, and `def`s whose body is sealed by the
+module system.
+-/
+
+@[expose] def exposedDef : Nat := 0
+def sealedDef : Nat := 1
+theorem aTheorem : 0 = 0 := rfl
+opaque anOpaque : Nat := 2
+axiom anAxiom : Nat
+inductive AnInductive where | mk
+
+run_cmd do
+  let env ← Lean.getEnv
+  unless env.hasExposedBody ``exposedDef do
+    throwError "`exposedDef` should have an exposed body"
+  for n in [``sealedDef, ``aTheorem, ``anOpaque, ``anAxiom, ``AnInductive, `nonexistent.name] do
+    if env.hasExposedBody n then
+      throwError "`{n}` should not have an exposed body"