From c0b628947ca51fbc5e2a635469b31b7a1ee41941 Mon Sep 17 00:00:00 2001 From: lengyijun Date: Tue, 18 Aug 2026 15:36:53 +0800 Subject: [PATCH] refactor: `abbrev open'` Change `open'` and `close` from `def` to `abbrev` in the untyped locally nameless lambda calculus basics. --- .../LocallyNameless/Untyped/Basic.lean | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean index d1e4543a4..700d21787 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.lean @@ -27,7 +27,7 @@ namespace Cslib universe u -variable {Var : Type u} [HasFresh Var] [DecidableEq Var] +variable {Var : Type u} namespace LambdaCalculus.LocallyNameless.Untyped @@ -65,11 +65,13 @@ lemma openRec_abs : M.abs⟦i ↝ s⟧ = M⟦i + 1 ↝ s⟧.abs := by rfl /-- Variable opening of the closest binding. -/ @[scoped grind =] -def open' {X} (e u):= @Term.openRec X 0 u e +abbrev open' {X} (e u):= @Term.openRec X 0 u e @[inherit_doc] scoped infixr:80 " ^ " => Term.open' +variable [DecidableEq Var] + /-- Variable closing, replacing a free `fvar x` with `bvar k` -/ @[scoped grind =] def closeRec (k : ℕ) (x : Var) : Term Var → Term Var @@ -81,11 +83,9 @@ def closeRec (k : ℕ) (x : Var) : Term Var → Term Var @[inherit_doc] scoped notation:68 e "⟦" k " ↜ " x "⟧"=> Term.closeRec k x e -variable {x : Var} - /-- Variable closing of the closest binding. -/ @[scoped grind =] -def close {Var} [DecidableEq Var] (e u):= @Term.closeRec Var _ 0 u e +abbrev close (e : Term Var) (u : Var) := Term.closeRec 0 u e @[inherit_doc] scoped infixr:80 " ^* " => Term.close @@ -113,7 +113,7 @@ def fv : Term Var → Finset Var section -omit [HasFresh Var] +variable {x : Var} {n : Term Var} lemma closeRec_bvar : (bvar i)⟦k ↜ x⟧ = bvar i := by rfl @@ -123,8 +123,6 @@ lemma closeRec_app : (app l r)⟦k ↜ x⟧ = app (l⟦k ↜ x⟧) (r⟦k ↜ x lemma closeRec_abs : t.abs⟦k ↜ x⟧ = t⟦k + 1 ↜ x⟧.abs := by rfl -variable {x : Var} {n : Term Var} - lemma subst_bvar : (bvar i : Term Var)[x := n] = bvar i := by rfl lemma subst_fvar : (fvar x')[x := n] = if x = x' then n else fvar x' := by rfl