betaStx — Mathlib

Lean4
/-- `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. -/
@[term_parser 1000]
public meta def betaStx : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Util.TermReduce.betaStx 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "beta% ") (ParserDescr.cat✝ `term 0))
Похожие утверждения