Documentation

Std.Tactic.Lint.Misc

Various linters #

This file defines several small linters.

A linter for checking whether a declaration has a namespace twice consecutively in its name.

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

    A linter for checking for unused arguments. We skip all declarations that contain sorry in their value.

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

      A linter for checking definition doc strings.

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

        A linter for checking theorem doc strings.

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

          A linter for checking whether the correct declaration constructor (definition or theorem) has been used.

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

            A linter for checking whether statements of declarations are well-typed.

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

              A linter for checking that there are no bad max u v universe levels. Checks whether all universe levels u in the type of d are "good". This means that u either occurs in a level of d by itself, or (recursively) with only other good levels. When this fails, usually this means that there is a level max u v, where neither u nor v occur by themselves in a level. It is ok if one of u or v never occurs alone. For example, (α : Type u) (β : Type (max u v)) is a occasionally useful method of saying that β lives in a higher universe level than α.

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

                A linter for checking that declarations aren't syntactic tautologies. Checks whether a lemma is a declaration of the form ∀ a b ... z, e₁ = e₂ where e₁ and e₂ are identical exprs. We call declarations of this form syntactic tautologies. Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving basic facts with rfl when elaboration results in a different term than the user intended.

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

                  Return a list of unused have/suffices/let_fun terms in an expression. This actually finds all beta-redexes.

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

                    A linter for checking that declarations don't have unused term mode have statements. We do not tag this as @[std_linter] so that it is not in the default linter set as it is slow and an uncommon problem.

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

                      A linter for checking if variables appearing on both sides of an iff are explicit. Ideally, such variables should be implicit instead.

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