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.