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