Skip to content

feat: Terminating FullEta - #822

Open
lengyijun wants to merge 1 commit into
leanprover:mainfrom
awesome-lambda-calculus:sn_fulleta
Open

lengyijun wants to merge 1 commit into
leanprover:mainfrom
awesome-lambda-calculus:sn_fulleta

Conversation

@lengyijun

@lengyijun lengyijun commented Aug 20, 2026 •

Copy link
Copy Markdown
Contributor

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

@lengyijun
lengyijun force-pushed the sn_fulleta branch 2 times, most recently from 39e7572 to 62f95ea Compare August 20, 2026 00:54
@lengyijun lengyijun changed the title feat: SN FullEta feat: Terminating FullEta Sep 3, 2026
@lengyijun
lengyijun force-pushed the sn_fulleta branch 3 times, most recently from 291470d to 666c02d Compare September 3, 2026 05:46
@lengyijun
lengyijun force-pushed the sn_fulleta branch 7 times, most recently from e9df2a9 to 7147bd6 Compare September 21, 2026 23:47
@lengyijun
lengyijun force-pushed the sn_fulleta branch 3 times, most recently from 3125fe7 to 9cd1f1c Compare September 28, 2026 00:15
@lengyijun
lengyijun force-pushed the sn_fulleta branch 2 times, most recently from a777c93 to 6b4e658 Compare October 5, 2026 00:29
@lengyijun
lengyijun requested a review from crei as a code owner October 5, 2026 00:29
@lengyijun
lengyijun force-pushed the sn_fulleta branch 2 times, most recently from 96cf9f1 to 7ec55da Compare October 13, 2026 01:27
Adds a size measure on untyped λ-terms and uses it to prove that η-reduction is terminating
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant