feat(scripts): @[expose] removal-candidate report pipeline (draft)#217

Draft

kim-em wants to merge 27 commits into

leanprover-community:nightly-testingfrom

kim-em:no_expose

Commits on May 8, 2026

feat(scripts): add @[expose] removal-candidate report pipeline

kim-em
and
claude
committed
chore(scripts): work around #guard_msgs / aesop failures in expose pipeline

kim-em
and
claude
committed

Commits on May 9, 2026

chore(scripts): widen expose-pipeline parser to include `[type_class] used instances`

kim-em
and
claude
committed
feat(scripts): add static-reference signal for @[expose] removal pipeline

kim-em
and
claude
committed
feat(scripts): track theorem-kind referencers + same-module rfl signal

kim-em
and
claude
committed

Commits on May 10, 2026

Commits on May 11, 2026

Commits on May 13, 2026

fix(scripts): section-strategy edit handles existing attribute blocks

kim-em
and
claude
committed