Skip to content

feat(locallynameless): Adds deriving DecidableEq to the Term - #825

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

feat(locallynameless): Adds deriving DecidableEq to the Term #825
lengyijun wants to merge 1 commit into
leanprover:mainfrom
awesome-lambda-calculus:decidableeq

feat: Adds deriving DecidableEq to the Term inductive type in the unt…

4ffda52
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
check-pr-title
succeeded Aug 20, 2026 in 3s