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.

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.

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.

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

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

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

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

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

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

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

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

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

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

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

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