refactor(Studies): disaggregate PIP — relocate to Studies, consume Core, Prop-native#21

Merged

hawkrobe merged 8 commits into

mainfrom

refactor/pip-disaggregate

May 30, 2026

Commits on May 30, 2026

refactor(Studies): move PIP framework from Semantics into KeshetAbney2024
hawkrobe
committed
refactor(Studies/KeshetAbney2024): make PIPExprF evaluators Prop-native
hawkrobe
committed
refactor(Studies/KeshetAbney2024): Prop-native PIP framework, consume boxR/diamondR
hawkrobe
committed
refactor(Studies/KeshetAbney2024): collapse PIP bridges onto Prop-native Core
hawkrobe
committed
refactor(Studies/KeshetAbney2024): Prop-native analysis files (Bool removed)
hawkrobe
committed
docs(Studies/KeshetAbney2024): refresh docstrings for Prop-native PIP
hawkrobe
committed
fix(Studies/KeshetAbney2024): reduce isWinner match via simp in winner_desc_empty
hawkrobe
committed
refactor(Studies/KeshetAbney2024): consume Core GQ, drop vacuous lemma, fix cites
hawkrobe
committed