fix: make theorem workspace generation robust to source context - #509

Merged

kim-em merged 5 commits into

leanprover:mainfrom

kim-em:codex/robust-statement-extraction

Aug 9, 2026

Commits on Aug 6, 2026

fix: make theorem workspace generation robust to source context
kim-em
committed
d942986
fix: derive delegation arguments from elaborated declarations
kim-em
committed
6936c3b

Commits on Aug 9, 2026

fix: derive delegation arguments from the declaration's signature only

kim-em
and
claude
committed
635ecc3
fix: trust the elaborated parameters only where they mean something

kim-em
and
claude
committed
b6da826
Merge branch 'main' into codex/robust-statement-extraction
kim-em
authored
61181e6