Skip to content

perf: skip re-attempting pending TC mvars with unchanged instantiated goals (quadratic resumption, #14448) - #14449

Open
grandchildrice wants to merge 1 commit into
leanprover:masterfrom
grandchildrice:t6-upstream
Open

perf: skip re-attempting pending TC mvars with unchanged instantiated goals (quadratic resumption, #14448)#14449
grandchildrice wants to merge 1 commit into
leanprover:masterfrom
grandchildrice:t6-upstream

perf: avoid quadratic re-attempts of pending TC mvars in synthesizeSy…

8607fed
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
check-stdlib-flags
succeeded Jul 19, 2026 in 3s