187a8c1ce3
This PR fixes a panic in `grind` where `sreifyCore?` could encounter power subterms not yet internalized in the E-graph during nested propagation. The ring reifier (`reifyCore?`) already had a defensive `alreadyInternalized` check before creating variables, but the semiring reifier (`sreifyCore?`) was missing this guard. When `propagatePower` decomposed `a ^ (b₁ + b₂)` into `a^b₁ * a^b₂` and the resulting terms triggered further propagation, the semiring reifier could be called on subterms not yet in the E-graph, causing `markTerm` to fail. Closes #12428 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| CMakeLists.txt | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||