feat(CombinatoryLogic): Partrec → SKI computability#403

Draft

jessealama wants to merge 7 commits intoleanprover:mainfrom

jessealama:ski-equivalence

Commits on Mar 21, 2026

feat(CombinatoryLogic): Partrec → SKI computability
jessealama
committed
refactor(CombinatoryLogic): simplify Computes using isChurch_trans
jessealama
committed
style(PartrecEquivalence): add blank lines after defs and clarify docstrings
jessealama
committed
style(CombinatoryLogic): trim docs, simplify proofs, fix naming conventions
jessealama
committed
refactor(CombinatoryLogic): rename PartrecEquivalence → PartrecToSKI
jessealama
committed
refactor(CombinatoryLogic): extract helpers, simplify proofs
jessealama
committed
refactor(PartrecToSKI): split rfind_eval_facts into two lemmas
jessealama
committed