def Lean.Meta.delta? (e : Expr) (p : Name → Bool := fun (x : Name) => true) : CoreM (Option Expr)

def Lean.Meta.deltaExpand (e : Expr) (p : Name → Bool) : CoreM Expr

Low-level delta expansion. It is used to implement equation lemmas and elimination principles for recursive definitions.

def Lean.MVarId.deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM MVarId

Delta expand declarations that satisfy p at mvarId type.

def Lean.MVarId.deltaLocalDecl (mvarId : MVarId) (fvarId : FVarId) (p : Name → Bool) : MetaM MVarId

Delta expand declarations that satisfy p at fvarId type.