Documentation

Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta

βη-Confluence for the λ-calculus #

Reference #

source
@[reducible, inline]
abbrev Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBetaEta {Var : Type u} :
Term Var → Term Var → Prop

Full βη-reduction.

Equations
Instances For
    source
    def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_⭢βηᶠ_» :
    Lean.TrailingParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.«term_↠βηᶠ_» :
      Lean.TrailingParserDescr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBetaEta.redex_app_l_cong {Var✝ : Type u_1} {M M' N : Term Var✝} (redex : Relation.ReflTransGen FullBetaEta M M') (lc_N : N.LC) :
        Relation.ReflTransGen FullBetaEta (M.app N) (M'.app N)
        source
        theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.FullBetaEta.redex_app_r_cong {Var✝ : Type u_1} {M M' N : Term Var✝} (redex : Relation.ReflTransGen FullBetaEta M M') (lc_N : N.LC) :
        Relation.ReflTransGen FullBetaEta (N.app M) (N.app M')