Documentation

Lean.Meta.Tactic.Delta

source
def Lean.Meta.delta? (e : Lean.Expr) (p : optParam (Lean.Name → Bool) fun x => true) :
Lean.CoreM (Option Lean.Expr)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.deltaExpand (e : Lean.Expr) (p : Lean.Name → Bool) :
Lean.CoreM Lean.Expr

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

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MVarId.deltaTarget (mvarId : Lean.MVarId) (p : Lean.Name → Bool) :
Lean.MetaM Lean.MVarId

Delta expand declarations that satisfy p at mvarId type.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.deltaTarget (mvarId : Lean.MVarId) (p : Lean.Name → Bool) :
Lean.MetaM Lean.MVarId
Equations
source
def Lean.MVarId.deltaLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (p : Lean.Name → Bool) :
Lean.MetaM Lean.MVarId

Delta expand declarations that satisfy p at fvarId type.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.deltaLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (p : Lean.Name → Bool) :
Lean.MetaM Lean.MVarId
Equations