simp? tactic

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

def Std.Tactic.simpTraceArgsRest : Lean.ParserDescr

The common arguments of simp? and simp?!.

Equations

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

def Std.Tactic.simpTrace : Lean.ParserDescr

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.

def Std.Tactic.tacticSimp?!_ : Lean.ParserDescr

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.

def Std.Tactic.mkSimpCallStx (stx : Lean.Syntax) (usedSimps : Lean.Meta.Simp.UsedSimps) : Lean.MetaM (Lean.TSyntax `tactic)

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

Equations

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

def Std.Tactic.simpAllTraceArgsRest : Lean.ParserDescr

The common arguments of simp_all? and simp_all?!.

Equations

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

def Std.Tactic.simpAllTrace : Lean.ParserDescr

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.

def Std.Tactic.tacticSimp_all?!_ : Lean.ParserDescr

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.

def Std.Tactic.dsimpTraceArgsRest : Lean.ParserDescr

The common arguments of dsimp? and dsimp?!.

Equations

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

def Std.Tactic.dsimpLocation' (ctx : Lean.Meta.Simp.Context) (loc : Lean.Elab.Tactic.Location) : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.UsedSimps

Implementation of dsimp.

Equations

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

def Std.Tactic.dsimpLocation'.go (ctx : Lean.Meta.Simp.Context) (fvarIdsToSimp : Array Lean.FVarId) (simplifyTarget : Bool) : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.UsedSimps

Implementation of dsimp.

Equations

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

def Std.Tactic.dsimpTrace : Lean.ParserDescr

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.

def Std.Tactic.tacticDsimp?!_ : Lean.ParserDescr

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.