Skip to content

feat: Add BetaAt uniqueness, FV preservation, and left redex-count bound - #800

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

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

Conversation

@lengyijun

@lengyijun lengyijun commented Aug 14, 2026 •

Copy link
Copy Markdown
Contributor

new theorems : BetaAt.step_fv BetaAt.unique BetaAt.lt_countRedexes Leftmost.steps_fv

@lengyijun

lengyijun commented Aug 14, 2026 •

Copy link
Copy Markdown
Contributor Author

A humble start of series of pr

@lengyijun

Copy link
Copy Markdown
Contributor Author

I have finished fokker_challenge, this is the only blocker

@lengyijun
lengyijun force-pushed the leftmost branch 5 times, most recently from 6951e55 to f474f82 Compare August 28, 2026 00:14
@lengyijun

Copy link
Copy Markdown
Contributor Author

@m-ow Could you please take a review ?

@lengyijun

lengyijun commented Sep 5, 2026 •

Copy link
Copy Markdown
Contributor Author

@lengyijun
lengyijun force-pushed the leftmost branch 2 times, most recently from 79baa2e to d960c47 Compare September 21, 2026 23:46
@lengyijun
lengyijun force-pushed the leftmost branch 3 times, most recently from 8c6b014 to fe77b95 Compare September 28, 2026 00:14
@lengyijun
lengyijun force-pushed the leftmost branch 2 times, most recently from 50578ac to 4771693 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 leftmost branch 3 times, most recently from 0691e31 to fb3b93b Compare October 14, 2026 04:56
new theorems : BetaAt.step_fv BetaAt.unique BetaAt.lt_countRedexes Leftmost.steps_fv
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