From 3af63fb895849a2640ba1d423b89f835d9c6c48f Mon Sep 17 00:00:00 2001 From: lengyijun Date: Mon, 10 Aug 2026 07:21:22 +0800 Subject: [PATCH] =?UTF-8?q?refactor:=20Replace=20=E2=86=94=20with=20=3D=20?= =?UTF-8?q?in=20`LcAt.lean`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit LcAt return bool, use `=` is more straightforward --- .../LambdaCalculus/LocallyNameless/Untyped/LcAt.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean index 4a74cf41d..754eb4181 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LcAt.lean @@ -67,11 +67,11 @@ theorem depth_open_fvar_eq_depth (M : Term Var) (x : Var) : depth (M ^ fvar x) = /-- Opening for some free variable at i-th bound variable, increments `LcAt`. -/ @[simp, scoped grind =] theorem lcAt_openRec_fvar_iff_lcAt (M : Term Var) (x : Var) (i : ℕ) : - LcAt i (M⟦i ↝ fvar x⟧) ↔ LcAt (i + 1) M := by + LcAt i (M⟦i ↝ fvar x⟧) = LcAt (i + 1) M := by induction M generalizing i <;> grind /-- Opening for some free variable is locally closed if and only if `M` is `LcAt 1`. -/ -theorem lcAt_open_fvar_iff_lcAt (M : Term Var) (x : Var) : LcAt 0 (M ^ fvar x) ↔ LcAt 1 M := +theorem lcAt_open_fvar_iff_lcAt (M : Term Var) (x : Var) : LcAt 0 (M ^ fvar x) = LcAt 1 M := lcAt_openRec_fvar_iff_lcAt M x 0 /-- Locally closed terms. -/