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

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

a82b30e
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 notice
check-pr-title
succeeded Oct 17, 2026 in 4s