simp? tactic

The simp? tactic is a simple wrapper around the simp with trace behavior.

def Lean.Elab.Tactic.mkSimpCallStx (stx : Syntax) (usedSimps : Meta.Simp.UsedSimps) : MetaM (TSyntax `tactic)

Constructs the syntax for a simp call, for use with simp?.

Equations

• Lean.Elab.Tactic.mkSimpCallStx stx usedSimps = do let a ← Lean.Elab.Tactic.mkSimpOnly stx.unsetTrailing usedSimps pure { raw := a }

def Lean.Elab.Tactic.evalSimpTrace : Tactic

Equations

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

def Lean.Elab.Tactic.evalSimpAllTrace : Tactic

Equations

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

def Lean.Elab.Tactic.dsimpLocation' (ctx : Meta.Simp.Context) (simprocs : Meta.Simp.SimprocsArray) (loc : Location) : TacticM Meta.Simp.Stats

Implementation of dsimp?.

Equations

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

def Lean.Elab.Tactic.dsimpLocation'.go (ctx : Meta.Simp.Context) (simprocs : Meta.Simp.SimprocsArray) (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Meta.Simp.Stats

Implementation of dsimp?.

Equations

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

def Lean.Elab.Tactic.evalDSimpTrace : Tactic

Equations

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