Documentation

Mathlib.Tactic.FunProp.Types

funProp #

this file defines environment extension for funProp

Indicated origin of a function or a statement.

Instances For

    Name of the origin.

    Equations
    Instances For

      Get the expression specified by origin.

      Equations
      Instances For

        Pretty print FunProp.Origin.

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

          Pretty print FunProp.Origin. Returns string unlike ppOrigin.

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

            Get origin of the head function.

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

              Default names to be considered reducible by fun_prop

              Equations
              Instances For

                fun_prop configuration

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

                  fun_prop state

                  • Simp's cache is used as the funProp tactic is designed to be used inside of simp and utilize its cache

                  • numSteps :

                    Count the number of steps and stop when maxSteps is reached.

                  • msgLog : List String

                    Log progress and failures messages that should be displayed to the user at the end.

                  Instances For

                    Log used theorem

                    Equations
                    • cfg.addThm thmId = { constToUnfold := cfg.constToUnfold, disch := cfg.disch, maxDepth := cfg.maxDepth, depth := cfg.depth, thmStack := thmId :: cfg.thmStack, maxSteps := cfg.maxSteps }
                    Instances For

                      Increase depth

                      Equations
                      • cfg.increaseDepth = { constToUnfold := cfg.constToUnfold, disch := cfg.disch, maxDepth := cfg.maxDepth, depth := cfg.depth + 1, thmStack := cfg.thmStack, maxSteps := cfg.maxSteps }
                      Instances For

                        Result of funProp, it is a proof of function property P f

                        Instances For

                          Check if previously used theorem was thmOrigin.

                          Equations
                          Instances For

                            Puts the theorem to the stack of used theorems.

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

                              Get predicate on names indicating if theys shoulds be unfolded.

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

                                Increase heartbeat, throws error when maxSteps was reached

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

                                  Log error message that will displayed to the user at the end.

                                  Equations
                                  Instances For