From 8b09366c787938d4e47c19088ba3d73d2f395c61 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sat, 6 Sep 2025 18:32:10 +0200 Subject: [PATCH] fix: casesOnSameCtor: export if not private (#10273) This PR tries to do the right thing about the visibility of the same-ctor-match-construct. --- .../Meta/Constructions/CasesOnSameCtor.lean | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/Lean/Meta/Constructions/CasesOnSameCtor.lean b/src/Lean/Meta/Constructions/CasesOnSameCtor.lean index b3f2f74c23..703f1081e6 100644 --- a/src/Lean/Meta/Constructions/CasesOnSameCtor.lean +++ b/src/Lean/Meta/Constructions/CasesOnSameCtor.lean @@ -95,13 +95,14 @@ public def mkCasesOnSameCtorHet (declName : Name) (indName : Name) : MetaM Unit let e := mkApp e (← mkEqSymm heq) mkLambdaFVars (params ++ #[motive] ++ ism1 ++ ism2 ++ #[heq] ++ alts) e - addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe - (name := declName) - (levelParams := casesOnInfo.levelParams) - (type := (← inferType e)) - (value := e) - (hints := ReducibilityHints.abbrev) - )) + withExporting (isExporting := !isPrivateName declName) do + addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe + (name := declName) + (levelParams := casesOnInfo.levelParams) + (type := (← inferType e)) + (value := e) + (hints := ReducibilityHints.abbrev) + )) modifyEnv fun env => markAuxRecursor env declName modifyEnv fun env => addToCompletionBlackList env declName modifyEnv fun env => addProtected env declName @@ -229,7 +230,8 @@ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit := discrInfos := #[{}, {}, {}]} -- Compare attributes with `mkMatcherAuxDefinition` - addDecl decl + withExporting (isExporting := !isPrivateName declName) do + addDecl decl Elab.Term.elabAsElim.setTag declName Match.addMatcherInfo declName matcherInfo setInlineAttribute declName