simp? tactic

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

def Lean.Elab.Tactic.filterSuggestionsAndLocalsFromSimpConfig (cfg : TSyntax `Lean.Parser.Tactic.optConfig) : MetaM (TSyntax `Lean.Parser.Tactic.optConfig)

Filter out +suggestions and +locals from the config syntax

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?.

def Lean.Elab.Tactic.evalSimpTrace : Tactic

def Lean.Elab.Tactic.evalSimpAllTrace : Tactic

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

Implementation of dsimp?.

def Lean.Elab.Tactic.evalDSimpTrace : Tactic