fix: handle non-internalized terms in semiring reifier 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 Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.