simp? tactic

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

def Lean.Elab.Tactic.mkSimpCallStx (stx : Lean.Syntax) (usedSimps : Lean.Meta.Simp.UsedSimps) : Lean.MetaM (Lean.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 : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.evalSimpAllTrace : Lean.Elab.Tactic.Tactic

Equations

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

def Lean.Elab.Tactic.dsimpLocation' (ctx : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (loc : Lean.Elab.Tactic.Location) : Lean.Elab.Tactic.TacticM Lean.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 : Lean.Meta.Simp.Context) (simprocs : Lean.Meta.Simp.SimprocsArray) (fvarIdsToSimp : Array Lean.FVarId) (simplifyTarget : Bool) : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Stats

Implementation of dsimp?.

Equations

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

def Lean.Elab.Tactic.evalDSimpTrace : Lean.Elab.Tactic.Tactic

Equations

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