Documentation

Batteries.Tactic.Lint.Simp

Linter for simplification lemmas #

This files defines several linters that prevent common mistakes when declaring simp lemmas:

The data associated to a simp theorem.

  • The hypotheses of the theorem

  • isConditional : Bool

    True if this is a conditional rewrite rule

  • lhs : Lean.Expr

    The thing to replace

  • rhs : Lean.Expr

    The result of replacement

Instances For

    Given the list of hypotheses, is this a conditional rewrite rule?

    Equations
    Instances For

      Runs the continuation on all the simp theorems encoded in the given type.

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

        Checks whether two expressions are equal for the simplifier. That is, they are reducibly-definitional equal, and they have the same head symbol.

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

          Constructs a message from all the simp theorems encoded in the given type.

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

            Returns true if this is a @[simp] declaration.

            Equations
            Instances For

              Returns the list of elements in the discrimination tree.

              Equations
              Instances For

                Returns the list of elements in the trie.

                Add message msg to any errors thrown inside k.

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

                  Render the list of simp lemmas.

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

                    A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire.

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

                      A linter for simp lemmas whose lhs has a variable as head symbol, and which hence never fire.

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

                        A linter for commutativity lemmas that are marked simp.

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