From 4ffda52680a2a2f36f667053ee0ddcc6e61bce6a Mon Sep 17 00:00:00 2001 From: lengyijun Date: Thu, 20 Aug 2026 12:30:37 +0800 Subject: [PATCH] feat: Adds deriving DecidableEq to the Term inductive type in the untyped lambda calculus (locally nameless) basic definitions Give Term Var an automatic decidable equality instance, so equality between terms can be decided computationally --- .../Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean index d1e4543a4..d3a1aa1c8 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean @@ -41,6 +41,7 @@ inductive Term (Var : Type u) | abs : Term Var → Term Var /-- Function application. -/ | app : Term Var → Term Var → Term Var +deriving DecidableEq namespace Term