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.mkSimpCallStx (stx : Syntax) (usedSimps : Meta.Simp.UsedSimps) :
MetaM (TSyntax `tactic)

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

Equations
    Instances For
      source
      def Lean.Elab.Tactic.evalSimpTrace :
      Tactic
      Equations
        Instances For
          source
          def Lean.Elab.Tactic.evalSimpAllTrace :
          Tactic
          Equations
            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?.

              Equations
                Instances For
                  source
                  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
                    Instances For
                      source
                      def Lean.Elab.Tactic.evalDSimpTrace :
                      Tactic
                      Equations
                        Instances For