# Term elaborators for reduction #

The `beta% f x1 ... xn` term elaborator elaborates the expression `f x1 ... xn` and then does one level of beta reduction. That is, if `f` is a lambda then it will substitute its arguments.

The purpose of this is to support substitutions in notations such as `∀ i, beta% p i` so that `p i` gets beta reduced when `p` is a lambda.

source
def Mathlib.Util.TermReduce.betaStx :
Lean.ParserDescr

`beta% t` elaborates `t` and then if the result is in the form `f x1 ... xn` where `f` is a (nested) lambda expression, it will substitute all of its arguments by beta reduction. This does not recursively do beta reduction, nor will it do beta reduction of subexpressions.

In particular, `t` is elaborated, its metavariables are instantiated, and then `Lean.Expr.headBeta` is applied.

Equations

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

Instances For

source
def Mathlib.Util.TermReduce.elabBeta :
Lean.Elab.Term.TermElab

`beta% t` elaborates `t` and then if the result is in the form `f x1 ... xn` where `f` is a (nested) lambda expression, it will substitute all of its arguments by beta reduction. This does not recursively do beta reduction, nor will it do beta reduction of subexpressions.

In particular, `t` is elaborated, its metavariables are instantiated, and then `Lean.Expr.headBeta` is applied.

Equations

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

Instances For

source
def Mathlib.Util.TermReduce.deltaStx :
Lean.ParserDescr

`delta% t` elaborates to a head-delta reduced version of `t`.

Equations

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

Instances For

source
def Mathlib.Util.TermReduce.elabDelta :
Lean.Elab.Term.TermElab

`delta% t` elaborates to a head-delta reduced version of `t`.

Equations

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

Instances For

source
def Mathlib.Util.TermReduce.zetaStx :
Lean.ParserDescr

`zeta% t` elaborates to a zeta and zeta-delta reduced version of `t`.

Equations

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

Instances For

source
def Mathlib.Util.TermReduce.elabZeta :
Lean.Elab.Term.TermElab

`zeta% t` elaborates to a zeta and zeta-delta reduced version of `t`.

Equations

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

Instances For

source
def Mathlib.Util.TermReduce.reduceProjStx :
Lean.ParserDescr

`reduceProj% t` apply `Expr.reduceProjStruct?` to all subexpressions of `t`.

Equations

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

Instances For

source
def Mathlib.Util.TermReduce.elabReduceProj :
Lean.Elab.Term.TermElab

`reduceProj% t` apply `Expr.reduceProjStruct?` to all subexpressions of `t`.

Equations

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

Instances For