b2aec782eb
This PR fixes an issue where `realizeConst` would generate auxiliary declarations (like `_sparseCasesOn`) using the original defining module's private name prefix rather than the realizing module's prefix. When two modules independently realized the same imported constant, they produced identically-named auxiliary declarations, causing "environment already contains" errors on diamond import. The fix re-privatizes the constant name under the current module before passing it to `withDeclNameForAuxNaming`, ensuring each realizing module generates distinctly named auxiliary declarations. Fixes #12825 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
5 lines
74 B
Text
5 lines
74 B
Text
import Lake
|
|
open Lake DSL
|
|
|
|
package repro
|
|
@[default_target] lean_lib Repro
|