Documentation

Std.Tactic.Lint.Simp

Linter for simplification lemmas #

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

  • 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

The data associated to a simp theorem.

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.

      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.

        Instances For

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

          Instances For

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

            Instances For

              Returns the list of elements in the discrimination tree.

              Instances For

                Returns the list of elements in the trie.

                Add message msg to any errors thrown inside k.

                Instances For

                  Render the list of simp lemmas.

                  Instances For

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

                    Instances For

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

                      Instances For

                        A linter for commutativity lemmas that are marked simp.

                        Instances For