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>
14 lines
340 B
Text
14 lines
340 B
Text
import Lean
|
|
|
|
open Lean Lean.Meta
|
|
|
|
inductive Nested where
|
|
| c : List Nested → Nested
|
|
|
|
run_meta show MetaM Unit from do
|
|
let env ← getEnv
|
|
let consts := env.constants.map₂.foldl (init := ∅) fun consts n info =>
|
|
consts.insert n info
|
|
let some importEnv := env.importEnv?
|
|
| unreachable!
|
|
let _ ← importEnv.replay consts
|