From 8df968de01f526d2f7aa113cc2d3231c5ee2c9db Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 15 Sep 2025 11:10:56 +0200
Subject: [PATCH] feat: have `example` default to the private scope (#10168)

---
 src/Lean/Elab/MutualDef.lean                  | 23 ++++++++++---------
 src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean |  8 +++++--
 tests/pkg/module/Module/Basic.lean            | 15 ++++++++++++
 3 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index a65bd1566f..9a467480d4 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -1189,7 +1189,10 @@ where
     let tacPromises ← views.mapM fun _ => IO.Promise.new
     let expandedDeclIds ← views.mapM fun view => withRef view.headerRef do
       Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
-    withExporting (isExporting := !expandedDeclIds.all (isPrivateName ·.declName)) do
+    withExporting (isExporting :=
+      -- `example`s are always private unless explicitly marked `public`
+      views.any (fun view => view.kind != .example || view.modifiers.isPublic) &&
+      expandedDeclIds.any (!isPrivateName ·.declName)) do
     let headers ← elabHeaders views expandedDeclIds bodyPromises tacPromises
     let headers ← levelMVarToParamHeaders views headers
     if let (#[view], #[declId]) := (views, expandedDeclIds) then
@@ -1278,7 +1281,7 @@ where
     }
     applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking
     applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
-  finishElab headers (isExporting := false) := withFunLocalDecls headers fun funFVars => do
+  finishElab headers := withFunLocalDecls headers fun funFVars => do
     let env ← getEnv
     if warn.exposeOnPrivate.get (← getOptions) then
       if env.header.isModule && !env.isExporting then
@@ -1288,15 +1291,13 @@ where
               logWarningAt attr.stx m!"Redundant `[expose]` attribute, it is meaningful on public \
                 definitions only"
 
-    withExporting (isExporting :=
-      headers.any (fun header =>
-        header.modifiers.isInferredPublic env &&
-        !header.modifiers.isMeta &&
-        !header.modifiers.attrs.any (·.name == `no_expose)) &&
-      (isExporting ||
-       headers.all (fun header => (header.kind matches .abbrev | .instance)) ||
-       (headers.all (·.kind == .def) && sc.attrs.any (· matches `(attrInstance| expose))) ||
-       headers.any (·.modifiers.attrs.any (·.name == `expose)))) do
+    withoutExporting (when :=
+      headers.all (fun header =>
+        header.modifiers.isMeta ||
+        header.modifiers.attrs.any (·.name == `no_expose) ||
+        (!(header.kind == .def && sc.attrs.any (· matches `(attrInstance| expose))) &&
+         !header.modifiers.attrs.any (·.name == `expose) &&
+         !header.kind matches .abbrev | .instance))) do
     let headers := headers.map fun header =>
       { header with modifiers.attrs := header.modifiers.attrs.filter (!·.name ∈ [`expose, `no_expose]) }
     let values ← try
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index 0c3e7e0ede..eb20f55fb2 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -149,9 +149,13 @@ def isGenPattern? (pat : Expr) : Option (GenPatternInfo × Expr) :=
 
 /-- Returns `true` if `declName` is the name of a `match`-expression congruence equation. -/
 def isMatchCongrEqDeclName (declName : Name) : CoreM Bool := do
-  let declName := privateToUserName declName
   match declName with
-  | .str p s => return (← isMatcher p) && Match.isCongrEqnReservedNameSuffix s
+  | .str p s =>
+    pure (Match.isCongrEqnReservedNameSuffix s) <&&>
+      -- `declName` was formed by `mkPrivateName _ matcherName` but as `matcherName` may or may not
+      -- have already been private, there is no direct way to invert this function; so we try both
+      -- possibilities (at most one of them can exist).
+      (isMatcher p <||> isMatcher (privateToUserName p))
   | _ => return false
 
 /-- Returns `true` if `e` is a constant for a `match`-expression congruence equation. -/
diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean
index b184e01761..43912be673 100644
--- a/tests/pkg/module/Module/Basic.lean
+++ b/tests/pkg/module/Module/Basic.lean
@@ -41,6 +41,20 @@ public theorem t : f = 1 := testSorry
 /-- A private definition. -/
 def fpriv := 1
 
+public section
+/-- Examples are always private. -/
+example : fpriv = 1 := rfl
+
+/--
+error: Unknown identifier `fpriv`
+
+Note: A private declaration `fpriv` (from the current module) exists but would need to be public to access here.
+-/
+#guard_msgs in
+/-- ...unless explicitly marked `public`. -/
+public example : fpriv = 1 := rfl
+end
+
 /--
 error: Unknown identifier `fpriv`
 
@@ -54,6 +68,7 @@ public class X
 /-- A local instance of a public class. -/
 instance : X := ⟨⟩
 
+
 -- Check that the theorem types are checked in exported context, where `f` is not defeq to `1`
 -- (but `fexp` is)