@[reducible, inline]
Full βη-reduction.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.stronglyCommute_eta_beta
{Var : Type u}
[HasFresh Var]
[DecidableEq Var]
:
η-reduction and β-reduction strongly commute.
theorem
Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.confluent_beta_eta
{Var : Type u}
[HasFresh Var]
[DecidableEq Var]
:
βη-reduction is confluent.