Documentation

Lean.Meta.Tactic.Rewrites

Extract the lemma, with arguments, that was used to produce a RewriteResult.

Equations
Instances For

    Weight to multiply the "specificity" of a rewrite lemma by when rewriting forwards.

    Equations
    Instances For

      Weight to multiply the "specificity" of a rewrite lemma by when rewriting backwards.

      Equations
      Instances For

        Configuration for DiscrTree.

        Equations
        Instances For

          Select = and local hypotheses.

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

            We drop .star and Eq * * * from the discriminator trees because they match too much.

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

              Create function for finding relevant declarations.

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

                Data structure recording a potential rewrite to report from the rw? tactic.

                • expr : Lean.Expr

                  The lemma we rewrote by. This is Expr, not just a Name, as it may be a local hypothesis.

                • symm : Bool

                  True if we rewrote backwards (i.e. with rw [← h]).

                • weight : Nat

                  The "weight" of the rewrite. This is calculated based on how specific the rewrite rule was.

                • The result from the rw tactic.

                • The metavariable context after the rewrite. This needs to be stored as part of the result so we can backtrack the state.

                • rfl? : Bool
                Instances For

                  Check to see if this expression (which must be a type) can be closed by with_reducible rfl.

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

                    Should we try discharging side conditions? If so, using assumption, or solve_by_elim?

                    Instances For

                      Shortcut for calling solveByElim.

                      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

                          Find keys which match the expression, or some subexpression.

                          Note that repeated subexpressions will be visited each time they appear, making this operation potentially very expensive. It would be good to solve this problem!

                          Implementation: we reverse the results from getMatch, so that we return lemmas matching larger subexpressions first, and amongst those we return more specific lemmas first.

                          Find lemmas which can rewrite the goal.

                          See also rewrites for a more convenient interface.

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

                                  Find lemmas which can rewrite the goal.

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