Documentation

Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEtaConfluence

βη-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.stronglyCommute_eta_beta {Var : Type u} [HasFresh Var] [DecidableEq Var] :
        Relation.StronglyCommute FullEta FullBeta

        η-reduction and β-reduction strongly commute.

        source
        theorem Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.confluent_beta_eta {Var : Type u} [HasFresh Var] [DecidableEq Var] :
        Relation.Confluent FullBetaEta

        βη-reduction is confluent.