η-reduction for the λ-calculus

inductive Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta {Var : Type u} : Term Var → Term Var → Prop

A single η-reduction step.

• eta {Var : Type u} {M : Term Var} : M.LC → (M.app (bvar 0)).abs.FullEta M

  The eta rule: λx. M x ⟶ M, provided x is not free in M.

• appL {Var : Type u} {Z M N : Term Var} : Z.LC → M.FullEta N → (Z.app M).FullEta (Z.app N)

  Left congruence rule for application.

• appR {Var : Type u} {Z M N : Term Var} : Z.LC → M.FullEta N → (M.app Z).FullEta (N.app Z)

  Right congruence rule for application.

• abs {Var : Type u} {M N : Term Var} (xs : Finset Var) : (∀ x ∉ xs, (M.open' (fvar x)).FullEta (N.open' (fvar x))) → M.abs.FullEta N.abs

  Congruence rule for lambda terms.

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_↠ηᶠ_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_⭢ηᶠ_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.step_lc_r {Var : Type u} {M M' : Term Var} (step : M.FullEta M') : M'.LC

The right side of an η-reduction is locally closed.

theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullEta.step_not_fv {Var : Type u} {M M' : Term Var} [HasFresh Var] [DecidableEq Var] {w : Var} (step : M.FullEta M') (hw : w ∉ M.fv) : w ∉ M'.fv

An η-reduction step does not introduce new free variables.