Definitional reduction steps

Single reduction steps on maximally shared terms, shared by Sym.dsimp, Sym.simp, and the grind normalizer. Each function returns none when the step does not apply, and a maximally shared term otherwise. The input and the output are definitionally equal.

def Lean.Meta.Sym.reduceBeta? (e : Expr) : SymM (Option Expr)

Beta-reduces e when its head is a lambda.

def Lean.Meta.Sym.reduceZeta? (e : Expr) : SymM (Option Expr)

Zeta-reduces the let/have telescope e: let x := v; b[x] becomes b[v].

def Lean.Meta.Sym.reduceZetaDelta? (e : Expr) (unfold : FVarId → Bool := fun (x : FVarId) => true) : SymM (Option Expr)

Unfolds the let-bound free variable at the head of e, where e is the variable itself or an application headed by it. The head position must be handled by the caller because the simplifiers do not visit application heads. Beta-reduction of the exposed lambda is left to reduceBeta?.

def Lean.Meta.Sym.reduceProjApp? (e : Expr) : SymM (Option Expr)

Reduces a projection function applied to a constructor, e.g. (a, b).1 to a. Class projections are not reduced; instances are handled by instance synthesis.

def Lean.Meta.Sym.reduceMatcherApp? (e : Expr) : SymM (Option Expr)

Iota-reduces a match or recursor application whose discriminants are constructors.