# Documentation

Std.Tactic.SimpTrace

# simp? tactic #

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

The common arguments of simp? and simp?!.

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

simp? takes the same arguments as simp, but reports an equivalent call to simp only that would be sufficient to close the goal. This is useful for reducing the size of the simp set in a local invocation to speed up processing.

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"


This command can also be used in simp_all and dsimp.

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

simp? takes the same arguments as simp, but reports an equivalent call to simp only that would be sufficient to close the goal. This is useful for reducing the size of the simp set in a local invocation to speed up processing.

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"


This command can also be used in simp_all and dsimp.

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

The common arguments of simp_all? and simp_all?!.

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

simp? takes the same arguments as simp, but reports an equivalent call to simp only that would be sufficient to close the goal. This is useful for reducing the size of the simp set in a local invocation to speed up processing.

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"


This command can also be used in simp_all and dsimp.

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

simp? takes the same arguments as simp, but reports an equivalent call to simp only that would be sufficient to close the goal. This is useful for reducing the size of the simp set in a local invocation to speed up processing.

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"


This command can also be used in simp_all and dsimp.

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

The common arguments of dsimp? and dsimp?!.

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

simp? takes the same arguments as simp, but reports an equivalent call to simp only that would be sufficient to close the goal. This is useful for reducing the size of the simp set in a local invocation to speed up processing.

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"


This command can also be used in simp_all and dsimp.

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

simp? takes the same arguments as simp, but reports an equivalent call to simp only that would be sufficient to close the goal. This is useful for reducing the size of the simp set in a local invocation to speed up processing.

example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
simp? -- prints "Try this: simp only [ite_true]"


This command can also be used in simp_all and dsimp.

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