`beta%`

term elaborator

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.

`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

- Mathlib.Util.TermBeta.betaStx = Lean.ParserDescr.node `Mathlib.Util.TermBeta.betaStx 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "beta% ") (Lean.ParserDescr.cat `term 0))

## Instances For

`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.