Documentation

Lean.Elab.Tactic.SimpTrace

simp? tactic #

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

source
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

Instances For
    source
    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?.

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

          Implementation of dsimp?.

          Instances For
            source
            def Lean.Elab.Tactic.evalDSimpTrace :
            Tactic
            Instances For