First, I am not sure whether this should be a RFC or a bug report. The current behavior is confusing and seemingly has no use cases, which is why I have opted for a bug report.

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Lemmas about private definitions are not private by default. One needs to add the private keyword explicitly.

Context

I keep forgetting that this is the current behavior, so I sometimes accidentally add non-private lemmas about private definitions to Mathlib, the latest in date being leanprover-community/mathlib4#15000.

Steps to Reproduce

Consider the following MWE

private def foo : Nat := 0

theorem foo_eq_zero : foo = 0 := rfl

#print foo -- `foo` is `private`
#print foo_eq_zero -- `foo_eq_zero` is not

Expected behavior: foo_eq_zero is private
Actual behavior: foo_eq_zero is not private

Versions

4.11.0-nightly-2024-08-11

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.