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.
Instances For
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.
Instances For
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.
Instances For
Constructs the syntax for a simp call, for use with simp?
.
Equations
- Std.Tactic.mkSimpCallStx stx usedSimps = let stx := Lean.Syntax.unsetTrailing stx; Lean.Internal.coeM (Lean.Elab.Tactic.mkSimpOnly stx usedSimps)
Instances For
The common arguments of simp_all?
and simp_all?!
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.
Instances For
The common arguments of dsimp?
and dsimp?!
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of dsimp
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implementation of dsimp
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.