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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.Sym.reduceZeta? (Lean.Expr.letE declName type v b nondep) = do let __do_lift ← Lean.Meta.Sym.reduceZeta?.go✝ (Lean.Expr.letE declName type v b nondep) #[] pure (some __do_lift)
• Lean.Meta.Sym.reduceZeta? e = pure none

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.