b7380758ae
This PR removes the obsolete `Lean.Environment.replay` from `src/Lean/Replay.lean` and replaces it with the improved version from `src/LeanChecker/Replay.lean`, which includes fixes for duplicate theorem handling and Quot/Eq dependency ordering. The primed names (`Replay'`, `replay'`) are renamed back to `Replay` and `replay`. A test for the original issue (nested inductives failing with `replay`) is added as `tests/elab/issue12819.lean`. Closes #12819 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| AddFalse.lean | ||
| AddFalse.lean.out.expected | ||
| AddFalseConstructor.lean | ||
| AddFalseConstructor.lean.out.expected | ||
| OpenPrivate.lean | ||
| PrivateConflictA.lean | ||
| PrivateConflictA2.lean | ||
| PrivateConflictB.lean | ||
| PrivateConflictB2.lean | ||
| PrivateConflictC.lean | ||
| PrivateConflictC.lean.fresh | ||
| PrivateConflictC.lean.out.expected | ||
| QuotEq.lean | ||
| ReplaceAxiom.lean | ||
| ReplaceAxiom.lean.out.expected | ||