def Lean.Elab.Tactic.deltaLocalDecl (declNames : Array Lake.Name) (fvarId : Lean.FVarId) : Lean.Elab.Tactic.TacticM Unit

Equations

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

def Lean.Elab.Tactic.deltaTarget (declNames : Array Lake.Name) : Lean.Elab.Tactic.TacticM Unit

Equations

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

def Lean.Elab.Tactic.evalDelta : Lean.Elab.Tactic.Tactic

"delta " ident+ (location)?

Equations

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