Skip to content

fix: preserve expected types of nested proofs - #14557

Draft
kernelpanic888 wants to merge 2 commits into
leanprover:masterfrom
kernelpanic888:codex/simp-hoisted-proof-14467
Draft

fix: preserve expected types of nested proofs#14557
kernelpanic888 wants to merge 2 commits into
leanprover:masterfrom
kernelpanic888:codex/simp-hoisted-proof-14467

fix: cache nested proofs by expected type

71cf855
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
check-awaiting-mathlib
succeeded Jul 26, 2026 in 4s