Documentation

Lean.Meta.Tactic.Simp.Rewrite

Wrapper for invoking discharge? method. It checks for maximum discharge depth, create trace nodes, and ensure the generated proof was successfully assigned to x.

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

            Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.

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

              For (← getConfig).index := true, use discrimination tree structure when collecting simp theorem candidates.

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

                For (← getConfig).index := false, Lean 3 style simp theorem retrieval. Only the root symbol is taken into account. Most of the structure of the discrimination tree is ignored.

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

                        Given a match-application e with MatcherInfo info, return some result if at least of one of the discriminants has been simplified.

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

                                      Discharge procedure for the ground/symbolic evaluator.

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

                                        Try to unfold ground term in the ground/symbolic evaluator.

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

                                              Invoke ground/symbolic evaluator from simp. It uses the seval theorems and simprocs.

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

                                                Try to unfold ground term in the ground/symbolic evaluator.

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

                                                      Return true if e is of the form (x : α) → ... → s = t → ... → False

                                                      Recall that this kind of proposition is generated by Lean when creating equations for functions and match-expressions with overlapping cases. Example: the following match-expression has overlapping cases.

                                                      def f (x y : Nat) :=
                                                        match x, y with
                                                        | Nat.succ n, Nat.succ m => ...
                                                        | _, _ => 0
                                                      

                                                      The second equation is of the form

                                                      (x y : Nat) → ((n m : Nat) → x = Nat.succ n → y = Nat.succ m → False) → f x y = 0
                                                      

                                                      The hypothesis (n m : Nat) → x = Nat.succ n → y = Nat.succ m → False is essentially saying the first case is not applicable.

                                                      Equations
                                                      Instances For

                                                        Tries to solve e using unifyEq?. It assumes that isEqnThmHypothesis e is true.

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