feat: Terminating FullEta by lengyijun · Pull Request #822 · leanprover/cslib

lengyijun · 2026-08-20T00:48:23Z

Adds a size measure on untyped λ-terms and uses it to prove that η-reduction is terminating

lengyijun requested review from chenson2018 and fmontesi as code owners August 20, 2026 00:48

lengyijun force-pushed the sn_fulleta branch 2 times, most recently from 39e7572 to 62f95ea Compare August 20, 2026 00:54

lengyijun force-pushed the sn_fulleta branch from 62f95ea to 390f3e8 Compare September 3, 2026 04:34

lengyijun changed the title ~~feat: SN FullEta~~ feat: Terminating FullEta Sep 3, 2026

lengyijun force-pushed the sn_fulleta branch 3 times, most recently from 291470d to 666c02d Compare September 3, 2026 05:46

lengyijun mentioned this pull request Sep 3, 2026

feat: sn_eta_steps_inv #860

Open

lengyijun force-pushed the sn_fulleta branch from 666c02d to 461b90a Compare September 15, 2026 10:43

lengyijun requested review from arademaker, kim-em and sorrachai as code owners September 15, 2026 10:43

lengyijun force-pushed the sn_fulleta branch 5 times, most recently from 6f44aaa to b8be9c6 Compare September 16, 2026 04:53

feat: Terminating FullEta

e9df2a9

Adds a size measure on untyped λ-terms and uses it to prove that η-reduction is terminating

lengyijun force-pushed the sn_fulleta branch from b8be9c6 to e9df2a9 Compare September 17, 2026 21:53

Navigation Menu